![]() |
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 131 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | bicom1 131 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | impbii 126 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: bicomd 141 bibi1i 228 bibi1d 233 ibibr 246 bibif 699 con2bidc 876 con2biddc 881 pm5.17dc 905 bigolden 957 nbbndc 1405 bilukdc 1407 falbitru 1428 3impexpbicom 1449 exists1 2134 eqcom 2191 abeq1 2299 necon2abiddc 2426 necon2bbiddc 2427 necon4bbiddc 2434 ssequn1 3320 axpow3 4195 isocnv 5833 suplocsrlem 7838 uzennn 10469 bezoutlemle 12044 |
Copyright terms: Public domain | W3C validator |