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 28128). After we define the constant
true ⊤ (df-tru 1531) and the constant false ⊥ (df-fal 1541), we
will be able to prove these truth table values:
((⊤ ∨ ⊤) ↔ ⊤) (truortru 1565), ((⊤ ∨ ⊥)
↔ ⊤)
(truorfal 1566), ((⊥ ∨ ⊤)
↔ ⊤) (falortru 1567), and
((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1568).
Contrast with ∧ (df-an 397), → (wi 4), ⊼ (df-nan 1476), and ⊻ (df-xor 1496). (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 841 | . 2 wff (𝜑 ∨ 𝜓) |
4 | 1 | wn 3 | . . 3 wff ¬ 𝜑 |
5 | 4, 2 | wi 4 | . 2 wff (¬ 𝜑 → 𝜓) |
6 | 3, 5 | wb 207 | 1 wff ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
This definition is referenced by: pm4.64 843 pm2.53 845 pm2.54 846 imor 847 ori 855 orri 856 ord 858 unitresl 866 orbi2d 909 orimdi 924 orbidi 946 pm5.6 995 ordi 999 pm5.17 1005 nanbi 1484 cador 1600 nf4 1779 19.43 1874 nfor 1896 19.32v 1932 19.32 2226 sbor 2308 dfsb3 2529 dfsb3ALT 2588 neor 3108 r19.30OLD 3339 r19.32v 3340 r19.43 3351 dfif2 4467 disjor 5038 soxp 7814 unxpwdom2 9041 cflim2 9674 cfpwsdom 9995 ltapr 10456 ltxrlt 10700 isprm4 16018 euclemma 16047 islpi 21687 restntr 21720 alexsubALTlem2 22586 alexsubALTlem3 22587 2bornot2b 28171 disjorf 30258 funcnv5mpt 30342 dvdszzq 30458 cycpm2tr 30689 ballotlemodife 31655 3orit 32843 dfon2lem5 32930 ecase13d 33559 elicc3 33563 nn0prpw 33569 onsucuni3 34531 orfa 35243 cnf1dd 35251 tsim1 35291 ineleq 35491 ifpidg 39737 ifpim123g 39746 ifpororb 39751 ifpor123g 39754 dfxor4 39991 df3or2 39993 frege83 40172 dffrege99 40188 frege131 40220 frege133 40222 pm10.541 40579 xrssre 41496 elprn2 41795 iundjiun 42623 r19.32 43177 |
Copyright terms: Public domain | W3C validator |