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 687 con2bidc 860 con2biddc 865 pm5.17dc 889 bigolden 939 nbbndc 1372 bilukdc 1374 falbitru 1395 3impexpbicom 1414 exists1 2095 eqcom 2141 abeq1 2249 necon2abiddc 2374 necon2bbiddc 2375 necon4bbiddc 2382 ssequn1 3246 axpow3 4101 isocnv 5712 suplocsrlem 7616 uzennn 10209 bezoutlemle 11696 |
Copyright terms: Public domain | W3C validator |