Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > bi2.04 | Unicode version |
Description: Logical equivalence of commuted antecedents. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
bi2.04 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.04 82 | . 2 | |
2 | pm2.04 82 | . 2 | |
3 | 1, 2 | impbii 125 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: imim21b 251 pm4.87 531 imimorbdc 866 sbcom2v 1938 mor 2019 r19.21t 2484 reu8 2853 ra5 2969 unissb 3736 reusv3 4351 zfregfr 4458 tfi 4466 fun11 5160 prime 9118 raluz2 9342 isprm3 11726 isprm4 11727 bj-inf2vnlem2 13096 |
Copyright terms: Public domain | W3C validator |