![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > bicom | GIF 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-1 5 ax-2 6 ax-mp 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 652 con2bidc 810 con2biddc 815 pm5.17dc 851 bigolden 904 nbbndc 1337 bilukdc 1339 falbitru 1360 3impexpbicom 1379 exists1 2051 eqcom 2097 abeq1 2204 necon2abiddc 2328 necon2bbiddc 2329 necon4bbiddc 2336 ssequn1 3185 axpow3 4033 isocnv 5628 bezoutlemle 11439 |
Copyright terms: Public domain | W3C validator |