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 672 con2bidc 845 con2biddc 850 pm5.17dc 874 bigolden 924 nbbndc 1357 bilukdc 1359 falbitru 1380 3impexpbicom 1399 exists1 2073 eqcom 2119 abeq1 2227 necon2abiddc 2351 necon2bbiddc 2352 necon4bbiddc 2359 ssequn1 3216 axpow3 4071 isocnv 5680 suplocsrlem 7584 uzennn 10177 bezoutlemle 11623 |
Copyright terms: Public domain | W3C validator |