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 751 | . 2 | |
2 | pm2.07 732 | . 2 | |
3 | 1, 2 | impbii 125 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wo 703 |
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 704 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm4.25 753 orordi 768 orordir 769 truortru 1400 falorfal 1403 truxortru 1414 falxorfal 1417 unidm 3270 preqsn 3760 reapirr 8489 reapti 8491 lt2msq 8795 nn0ge2m1nn 9188 absext 11020 prmdvdsexp 12095 sqpweven 12122 2sqpwodd 12123 |
Copyright terms: Public domain | W3C validator |