Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > oridm | Unicode version |
Description: Idempotent law for disjunction. Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 5-Aug-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 730 | . 2 | |
2 | pm2.07 711 | . 2 | |
3 | 1, 2 | impbii 125 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wo 682 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 683 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm4.25 732 orordi 747 orordir 748 truortru 1368 falorfal 1371 truxortru 1382 falxorfal 1385 unidm 3189 preqsn 3672 reapirr 8307 reapti 8309 lt2msq 8612 nn0ge2m1nn 9005 absext 10803 prmdvdsexp 11753 sqpweven 11780 2sqpwodd 11781 |
Copyright terms: Public domain | W3C validator |