![]() |
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 122 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | bicom1 122 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | impbii 117 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: bicomd 129 bibi1i 217 bibi1d 222 ibibr 235 bibif 613 con2bidc 768 con2biddc 773 pm5.17dc 809 bigolden 861 nbbndc 1282 bilukdc 1284 falbitru 1305 3impexpbicom 1324 exists1 1993 eqcom 2039 abeq1 2144 necon2abiddc 2265 necon2bbiddc 2266 necon4bbiddc 2273 ssequn1 3107 axpow3 3921 isocnv 5394 |
Copyright terms: Public domain | W3C validator |