![]() |
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 28206). After we define the constant
true ⊤ (df-tru 1541) and the constant false ⊥ (df-fal 1551), we
will be able to prove these truth table values:
((⊤ ∨ ⊤) ↔ ⊤) (truortru 1575), ((⊤ ∨ ⊥)
↔ ⊤)
(truorfal 1576), ((⊥ ∨ ⊤)
↔ ⊤) (falortru 1577), and
((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1578).
Contrast with ∧ (df-an 400), → (wi 4), ⊼ (df-nan 1483), and ⊻ (df-xor 1503). (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 844 | . 2 wff (𝜑 ∨ 𝜓) |
4 | 1 | wn 3 | . . 3 wff ¬ 𝜑 |
5 | 4, 2 | wi 4 | . 2 wff (¬ 𝜑 → 𝜓) |
6 | 3, 5 | wb 209 | 1 wff ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
This definition is referenced by: pm4.64 846 pm2.53 848 pm2.54 849 imor 850 ori 858 orri 859 ord 861 unitreslOLD 875 orbi2d 913 orimdi 928 orbidi 950 pm5.6 999 ordi 1003 pm5.17 1009 nanbi 1491 cador 1610 nf4 1789 19.43 1883 nfor 1905 19.32v 1941 19.32 2233 sbor 2312 dfsb3 2512 dfsb3ALT 2568 neor 3078 r19.32v 3294 r19.43 3304 dfif2 4427 disjor 5010 soxp 7806 unxpwdom2 9036 cflim2 9674 cfpwsdom 9995 ltapr 10456 ltxrlt 10700 isprm4 16018 euclemma 16047 islpi 21754 restntr 21787 alexsubALTlem2 22653 alexsubALTlem3 22654 2bornot2b 28249 disjorf 30342 funcnv5mpt 30431 dvdszzq 30557 cycpm2tr 30811 ballotlemodife 31865 3orit 33058 dfon2lem5 33145 ecase13d 33774 elicc3 33778 nn0prpw 33784 onsucuni3 34784 orfa 35520 cnf1dd 35528 tsim1 35568 ineleq 35768 ifpidg 40199 ifpim123g 40208 ifpororb 40213 ifpor123g 40216 dfxor4 40467 df3or2 40469 frege83 40647 dffrege99 40663 frege131 40695 frege133 40697 pm10.541 41071 xrssre 41980 elprn2 42276 iundjiun 43099 r19.32 43653 |
Copyright terms: Public domain | W3C validator |