![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > df-or | Unicode 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 (ex-or 25142). After we define the constant
true (df-tru 1398) and the constant false (df-fal 1401), we
will be able to prove these truth table values:
(truortru 1423),
(truorfal 1424), (falortru 1425), and
(falorfal 1426).
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 236.
This is the justification
for the definition, along with the fact that it introduces a new symbol
|
Ref | Expression |
---|---|
df-or |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 | |
2 | wps | . . 3 | |
3 | 1, 2 | wo 368 | . 2 |
4 | 1 | wn 3 | . . 3 |
5 | 4, 2 | wi 4 | . 2 |
6 | 3, 5 | wb 184 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: pm4.64 372 pm2.53 373 pm2.54 374 ori 375 orri 376 ord 377 imor 412 mtord 660 orbi2d 701 orimdi 847 ordi 864 pm5.17 888 pm5.6 912 orbidi 932 nanbi 1352 cador 1458 19.43 1693 19.32v 1730 nfor 1935 19.32 1967 dfsb3 2115 sbor 2139 neor 2781 r19.30 3002 r19.32v 3003 r19.43 3013 dfif2 3943 disjor 4436 sotric 4831 sotrieq 4832 isso2i 4837 soxp 6913 unxpwdom2 8035 cflim2 8664 cfpwsdom 8980 ltapr 9444 ltxrlt 9676 isprm4 14227 euclemma 14249 islpi 19650 restntr 19683 alexsubALTlem2 20548 alexsubALTlem3 20549 2bornot2b 25172 disjorf 27440 funcnv5mpt 27511 ballotlemodife 28436 3orit 29092 dfon2lem5 29219 ecase13d 30131 elicc3 30135 nn0prpw 30141 orfa 30479 unitresl 30482 cnf1dd 30490 tsim1 30537 pm10.541 31272 elprn2 31640 r19.32 32172 bj-ifim123g 37706 bj-ifidg 37707 bj-ifor123g 37725 bj-ifororb 37726 dfxor4 37789 |
Copyright terms: Public domain | W3C validator |