![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-or | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
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 2222 sbor 2297 dfsb3 2489 neor 3030 r19.43 3118 r19.32v 3187 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 34111 3orit 35304 dfon2lem5 35377 ecase13d 35791 elicc3 35795 nn0prpw 35801 onsucuni3 36840 orfa 37549 cnf1dd 37557 tsim1 37597 ineleq 37820 aks4d1p7 41548 safesnsupfilb 42842 ifpidg 42915 ifpim123g 42924 ifpororb 42929 ifpor123g 42932 dfxor4 43190 df3or2 43192 frege83 43370 dffrege99 43386 frege131 43418 frege133 43420 pm10.541 43798 xrssre 44724 elprn2 45016 iundjiun 45842 r19.32 46472 |
Copyright terms: Public domain | W3C validator |