![]() |
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 27853). After we define the constant
true ⊤ (df-tru 1605) and the constant false ⊥ (df-fal 1615), we
will be able to prove these truth table values:
((⊤ ∨ ⊤) ↔ ⊤) (truortru 1639), ((⊤ ∨ ⊥)
↔ ⊤)
(truorfal 1640), ((⊥ ∨ ⊤)
↔ ⊤) (falortru 1641), and
((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1642).
Contrast with ∧ (df-an 387), → (wi 4), ⊼ (df-nan 1558), and ⊻ (df-xor 1583). (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 836 | . 2 wff (𝜑 ∨ 𝜓) |
4 | 1 | wn 3 | . . 3 wff ¬ 𝜑 |
5 | 4, 2 | wi 4 | . 2 wff (¬ 𝜑 → 𝜓) |
6 | 3, 5 | wb 198 | 1 wff ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
This definition is referenced by: pm4.64 838 pm2.53 840 pm2.54 841 imor 842 ori 850 orri 851 ord 853 mtord 866 orbi2d 902 orimdi 917 orbidi 938 pm5.6 987 ordi 991 pm5.17 997 nanbi 1569 cador 1666 nf4 1831 19.43 1929 nfor 1951 19.32v 1983 19.32 2219 dfsb3 2450 sbor 2474 neor 3061 r19.30 3268 r19.32v 3269 r19.43 3279 dfif2 4309 disjor 4868 soxp 7571 unxpwdom2 8782 cflim2 9420 cfpwsdom 9741 ltapr 10202 ltxrlt 10447 isprm4 15802 euclemma 15829 islpi 21361 restntr 21394 alexsubALTlem2 22260 alexsubALTlem3 22261 2bornot2b 27895 disjorf 29955 funcnv5mpt 30033 ballotlemodife 31158 3orit 32193 dfon2lem5 32280 ecase13d 32896 elicc3 32900 nn0prpw 32906 onsucuni3 33810 orfa 34505 unitresl 34508 cnf1dd 34515 tsim1 34559 ineleq 34747 ifpidg 38794 ifpim123g 38803 ifpororb 38808 ifpor123g 38811 dfxor4 39015 df3or2 39017 frege83 39196 dffrege99 39212 frege131 39244 frege133 39246 pm10.541 39522 xrssre 40472 elprn2 40774 iundjiun 41601 r19.32 42126 |
Copyright terms: Public domain | W3C validator |