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 28200). After we define the constant
true ⊤ (df-tru 1540) and the constant false ⊥ (df-fal 1550), we
will be able to prove these truth table values:
((⊤ ∨ ⊤) ↔ ⊤) (truortru 1574), ((⊤ ∨ ⊥)
↔ ⊤)
(truorfal 1575), ((⊥ ∨ ⊤)
↔ ⊤) (falortru 1576), and
((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1577).
Contrast with ∧ (df-an 399), → (wi 4), ⊼ (df-nan 1482), and ⊻ (df-xor 1502). (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 843 | . 2 wff (𝜑 ∨ 𝜓) |
4 | 1 | wn 3 | . . 3 wff ¬ 𝜑 |
5 | 4, 2 | wi 4 | . 2 wff (¬ 𝜑 → 𝜓) |
6 | 3, 5 | wb 208 | 1 wff ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
This definition is referenced by: pm4.64 845 pm2.53 847 pm2.54 848 imor 849 ori 857 orri 858 ord 860 unitreslOLD 874 orbi2d 912 orimdi 927 orbidi 949 pm5.6 998 ordi 1002 pm5.17 1008 nanbi 1490 cador 1609 nf4 1788 19.43 1883 nfor 1905 19.32v 1941 19.32 2235 sbor 2316 dfsb3 2533 dfsb3ALT 2592 neor 3108 r19.30OLD 3339 r19.32v 3340 r19.43 3351 dfif2 4469 disjor 5046 soxp 7823 unxpwdom2 9052 cflim2 9685 cfpwsdom 10006 ltapr 10467 ltxrlt 10711 isprm4 16028 euclemma 16057 islpi 21757 restntr 21790 alexsubALTlem2 22656 alexsubALTlem3 22657 2bornot2b 28243 disjorf 30329 funcnv5mpt 30413 dvdszzq 30531 cycpm2tr 30761 ballotlemodife 31755 3orit 32945 dfon2lem5 33032 ecase13d 33661 elicc3 33665 nn0prpw 33671 onsucuni3 34651 orfa 35375 cnf1dd 35383 tsim1 35423 ineleq 35623 ifpidg 39906 ifpim123g 39915 ifpororb 39920 ifpor123g 39923 dfxor4 40160 df3or2 40162 frege83 40341 dffrege99 40357 frege131 40389 frege133 40391 pm10.541 40748 xrssre 41665 elprn2 41964 iundjiun 42791 r19.32 43345 |
Copyright terms: Public domain | W3C validator |