Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > oridm | Structured version Visualization version Unicode version |
Description: Idempotent law for disjunction. Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-1993.) (Proof shortened by Andrew Salmon, 16-Apr-2011.) (Proof shortened by Wolf Lammen, 10-Mar-2013.) |
Ref | Expression |
---|---|
oridm |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm1.2 535 | . 2 | |
2 | pm2.07 411 | . 2 | |
3 | 1, 2 | impbii 199 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 196 wo 383 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-or 385 |
This theorem is referenced by: pm4.25 537 orordi 552 orordir 553 truortru 1510 falorfal 1513 unidm 3756 preqsnd 4392 preqsn 4393 preqsnOLD 4394 suceloni 7013 tz7.48lem 7536 msq0i 10674 msq0d 10676 prmdvdsexp 15427 metn0 22165 rrxcph 23180 nb3grprlem2 26283 pdivsq 31635 pm11.7 38596 |
Copyright terms: Public domain | W3C validator |