df-or - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-or		Structured version Visualization version GIF version

Definition df-or 847

Description: Define disjunction (logical "or"). Definition of [Margaris] p. 49. When the left operand, right operand, or both are true, the result is true; when both sides are false, the result is false. For example, it is true that (2 = 3 ∨ 4 = 4) (ex-or 30224). After we define the constant true ⊤ (df-tru 1537) and the constant false ⊥ (df-fal 1547), we will be able to prove these truth table values: ((⊤ ∨ ⊤) ↔ ⊤) (truortru 1571), ((⊤ ∨ ⊥) ↔ ⊤) (truorfal 1572), ((⊥ ∨ ⊤) ↔ ⊤) (falortru 1573), and ((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1574).

Contrast with ∧ (df-an 396), → (wi 4), ⊼ (df-nan 1486), and ⊻ (df-xor 1506). (Contributed by NM, 27-Dec-1992.)

**Assertion**
Ref	Expression
df-or	⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))

**Detailed syntax breakdown of Definition df-or**
Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3	1, 2	wo 846	. 2 wff (𝜑 ∨ 𝜓)
4	1	wn 3	. . 3 wff ¬ 𝜑
5	4, 2	wi 4	. 2 wff (¬ 𝜑 → 𝜓)
6	3, 5	wb 205	1 wff ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))

Colors of variables: wff setvar class

This definition is referenced by: pm4.64 848 pm2.53 850 pm2.54 851 imor 852 ori 860 orri 861 ord 863 orbi2d 914 orimdi 929 orbidi 951 pm5.6 1000 ordi 1004 pm5.17 1010 nanbi 1494 cador 1602 nf4 1782 19.43 1878 nfor 1900 19.32v 1936 19.32 2219 sbor 2296 dfsb3 2488 neor 3029 r19.43 3117 r19.32v 3186 dfif2 4526 disjor 5122 soxp 8128 unxpwdom2 9605 cflim2 10280 cfpwsdom 10601 ltapr 11062 ltxrlt 11308 isprm4 16648 euclemma 16677 dvdszzq 16686 isdomn5 21242 islpi 23046 restntr 23079 alexsubALTlem2 23945 alexsubALTlem3 23946 2bornot2b 30267 disjorf 32362 funcnv5mpt 32447 cycpm2tr 32834 ballotlemodife 34107 3orit 35300 dfon2lem5 35373 ecase13d 35787 elicc3 35791 nn0prpw 35797 onsucuni3 36836 orfa 37544 cnf1dd 37552 tsim1 37592 ineleq 37815 aks4d1p7 41543 safesnsupfilb 42820 ifpidg 42893 ifpim123g 42902 ifpororb 42907 ifpor123g 42910 dfxor4 43168 df3or2 43170 frege83 43348 dffrege99 43364 frege131 43396 frege133 43398 pm10.541 43776 xrssre 44702 elprn2 44994 iundjiun 45820 r19.32 46450

W3C validator

	
		OSZAR »