![]() |
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 27408). After we define the constant
true ⊤ (df-tru 1526) and the constant false ⊥ (df-fal 1529), we
will be able to prove these truth table values:
((⊤ ∨ ⊤) ↔ ⊤) (truortru 1550), ((⊤ ∨ ⊥)
↔ ⊤)
(truorfal 1551), ((⊥ ∨ ⊤)
↔ ⊤) (falortru 1552), and
((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1553).
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 1488), and ⊻ (df-xor 1505) . (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 693 orbi2d 738 orimdi 910 ordi 926 pm5.17 950 pm5.6 971 orbidi 993 nanbi 1494 cador 1587 nf4 1753 19.43 1850 nfor 1874 19.32v 1909 19.32 2139 nforOLD 2280 dfsb3 2402 sbor 2426 neor 2914 r19.30 3111 r19.32v 3112 r19.43 3122 dfif2 4121 disjor 4666 soxp 7335 unxpwdom2 8534 cflim2 9123 cfpwsdom 9444 ltapr 9905 ltxrlt 10146 isprm4 15444 euclemma 15472 islpi 21001 restntr 21034 alexsubALTlem2 21899 alexsubALTlem3 21900 2bornot2b 27450 disjorf 29518 funcnv5mpt 29597 ballotlemodife 30687 3orit 31722 dfon2lem5 31816 ecase13d 32432 elicc3 32436 nn0prpw 32443 onsucuni3 33345 orfa 34011 unitresl 34014 cnf1dd 34022 tsim1 34067 ineleq 34259 ifpidg 38153 ifpim123g 38162 ifpororb 38167 ifpor123g 38170 dfxor4 38375 df3or2 38377 frege83 38557 dffrege99 38573 frege131 38605 frege133 38607 pm10.541 38883 xrssre 39877 elprn2 40184 iundjiun 40995 r19.32 41488 |
Copyright terms: Public domain | W3C validator |