Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > bicom | Unicode version |
Description: Commutative law for equivalence. Theorem *4.21 of [WhiteheadRussell] p. 117. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 11-Nov-2012.) |
Ref | Expression |
---|---|
bicom |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bicom1 130 | . 2 | |
2 | bicom1 130 | . 2 | |
3 | 1, 2 | impbii 125 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: bicomd 140 bibi1i 227 bibi1d 232 ibibr 245 bibif 688 con2bidc 865 con2biddc 870 pm5.17dc 894 bigolden 944 nbbndc 1383 bilukdc 1385 falbitru 1406 3impexpbicom 1425 exists1 2109 eqcom 2166 abeq1 2274 necon2abiddc 2400 necon2bbiddc 2401 necon4bbiddc 2408 ssequn1 3287 axpow3 4150 isocnv 5773 suplocsrlem 7740 uzennn 10361 bezoutlemle 11926 |
Copyright terms: Public domain | W3C validator |