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 26670). After we define the constant
true ⊤ (df-tru 1478) and the constant false ⊥ (df-fal 1481), we
will be able to prove these truth table values:
((⊤ ∨ ⊤) ↔ ⊤) (truortru 1501), ((⊤ ∨ ⊥)
↔ ⊤)
(truorfal 1502), ((⊥ ∨ ⊤)
↔ ⊤) (falortru 1503), and
((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1504).
This is our first use of the biconditional connective in a definition; we use the biconditional connective in place of the traditional "<=def=>", which means the same thing, except that we can manipulate the biconditional connective directly in proofs rather than having to rely on an informal definition substitution rule. Note that if we mechanically substitute (¬ 𝜑 → 𝜓) for (𝜑 ∨ 𝜓), we end up with an instance of previously proved theorem biid 250. This is the justification for the definition, along with the fact that it introduces a new symbol ∨. Contrast with ∧ (df-an 385), → (wi 4), ⊼ (df-nan 1440), and ⊻ (df-xor 1457) . (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 382 | . 2 wff (𝜑 ∨ 𝜓) |
4 | 1 | wn 3 | . . 3 wff ¬ 𝜑 |
5 | 4, 2 | wi 4 | . 2 wff (¬ 𝜑 → 𝜓) |
6 | 3, 5 | wb 195 | 1 wff ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
This definition is referenced by: pm4.64 386 pm2.53 387 pm2.54 388 ori 389 orri 390 ord 391 imor 427 mtord 690 orbi2d 734 orimdi 888 ordi 904 pm5.17 928 pm5.6 949 orbidi 969 nanbi 1446 cador 1538 nf4 1704 19.43 1799 nfor 1822 19.32v 1856 19.32 2088 nforOLD 2232 dfsb3 2362 sbor 2386 neor 2873 r19.30 3063 r19.32v 3064 r19.43 3074 dfif2 4038 disjor 4567 soxp 7177 unxpwdom2 8376 cflim2 8968 cfpwsdom 9285 ltapr 9746 ltxrlt 9987 isprm4 15235 euclemma 15263 islpi 20763 restntr 20796 alexsubALTlem2 21662 alexsubALTlem3 21663 2bornot2b 26712 disjorf 28774 funcnv5mpt 28852 ballotlemodife 29886 3orit 30851 dfon2lem5 30936 ecase13d 31477 elicc3 31481 nn0prpw 31488 bj-nf4 31768 onsucuni3 32391 orfa 33051 unitresl 33054 cnf1dd 33062 tsim1 33107 ifpidg 36855 ifpim123g 36864 ifpororb 36869 ifpor123g 36872 dfxor4 37077 df3or2 37079 frege83 37260 dffrege99 37276 frege131 37308 frege133 37310 pm10.541 37588 xrssre 38505 elprn2 38701 iundjiun 39353 r19.32 39816 |
Copyright terms: Public domain | W3C validator |