![]() |
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 27581). After we define the constant
true ⊤ (df-tru 1627) and the constant false ⊥ (df-fal 1630), we
will be able to prove these truth table values:
((⊤ ∨ ⊤) ↔ ⊤) (truortru 1651), ((⊤ ∨ ⊥)
↔ ⊤)
(truorfal 1652), ((⊥ ∨ ⊤)
↔ ⊤) (falortru 1653), and
((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1654).
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 251. 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 1589), and ⊻ (df-xor 1606) . (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 196 | 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 695 orbi2d 740 orimdi 928 ordi 944 pm5.17 968 pm5.6 989 orbidi 1011 nanbi 1595 cador 1688 nf4 1854 19.43 1951 nfor 1975 19.32v 2010 19.32 2240 nforOLD 2381 dfsb3 2503 sbor 2527 neor 3015 r19.30 3212 r19.32v 3213 r19.43 3223 dfif2 4224 disjor 4778 soxp 7450 unxpwdom2 8650 cflim2 9269 cfpwsdom 9590 ltapr 10051 ltxrlt 10292 isprm4 15591 euclemma 15619 islpi 21147 restntr 21180 alexsubALTlem2 22045 alexsubALTlem3 22046 2bornot2b 27623 disjorf 29691 funcnv5mpt 29770 ballotlemodife 30860 3orit 31895 dfon2lem5 31989 ecase13d 32605 elicc3 32609 nn0prpw 32616 onsucuni3 33518 orfa 34186 unitresl 34189 cnf1dd 34197 tsim1 34242 ineleq 34434 ifpidg 38330 ifpim123g 38339 ifpororb 38344 ifpor123g 38347 dfxor4 38552 df3or2 38554 frege83 38734 dffrege99 38750 frege131 38782 frege133 38784 pm10.541 39060 xrssre 40054 elprn2 40361 iundjiun 41172 r19.32 41665 |
Copyright terms: Public domain | W3C validator |