![]() |
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 131 | . 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑)) | |
2 | bicom1 131 | . 2 ⊢ ((𝜓 ↔ 𝜑) → (𝜑 ↔ 𝜓)) | |
3 | 1, 2 | impbii 126 | 1 ⊢ ((𝜑 ↔ 𝜓) ↔ (𝜓 ↔ 𝜑)) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 |
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 956 nbbndc 1404 bilukdc 1406 falbitru 1427 3impexpbicom 1448 exists1 2133 eqcom 2190 abeq1 2298 necon2abiddc 2425 necon2bbiddc 2426 necon4bbiddc 2433 ssequn1 3319 axpow3 4191 isocnv 5827 suplocsrlem 7824 uzennn 10453 bezoutlemle 12026 |
Copyright terms: Public domain | W3C validator |