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 547 imimorbdc 882 sbcom2v 1965 mor 2048 r19.21t 2532 reu8 2908 ra5 3025 unissb 3803 reusv3 4421 zfregfr 4534 tfi 4542 fun11 5238 prime 9264 raluz2 9491 isprm3 11999 isprm4 12000 bj-inf2vnlem2 13588 |
Copyright terms: Public domain | W3C validator |