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 28781). After we define the constant
true ⊤ (df-tru 1545) and the constant false ⊥ (df-fal 1555), we
will be able to prove these truth table values:
((⊤ ∨ ⊤) ↔ ⊤) (truortru 1579), ((⊤ ∨ ⊥)
↔ ⊤)
(truorfal 1580), ((⊥ ∨ ⊤)
↔ ⊤) (falortru 1581), and
((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1582).
Contrast with ∧ (df-an 397), → (wi 4), ⊼ (df-nan 1487), and ⊻ (df-xor 1507). (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 205 | 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 1495 cador 1614 nf4 1794 19.43 1889 nfor 1911 19.32v 1947 19.32 2230 sbor 2308 dfsb3 2500 neor 3038 r19.32v 3270 r19.43 3280 dfif2 4467 disjor 5059 soxp 7961 unxpwdom2 9325 cflim2 10020 cfpwsdom 10341 ltapr 10802 ltxrlt 11046 isprm4 16387 euclemma 16416 islpi 22298 restntr 22331 alexsubALTlem2 23197 alexsubALTlem3 23198 2bornot2b 28824 disjorf 30914 funcnv5mpt 31001 dvdszzq 31125 cycpm2tr 31382 ballotlemodife 32460 3orit 33654 dfon2lem5 33759 ecase13d 34498 elicc3 34502 nn0prpw 34508 onsucuni3 35534 orfa 36236 cnf1dd 36244 tsim1 36284 ineleq 36482 aks4d1p7 40088 isdomn5 40168 ifpidg 41077 ifpim123g 41086 ifpororb 41091 ifpor123g 41094 dfxor4 41344 df3or2 41346 frege83 41524 dffrege99 41540 frege131 41572 frege133 41574 pm10.541 41955 xrssre 42858 elprn2 43146 iundjiun 43969 r19.32 44558 |
Copyright terms: Public domain | W3C validator |