![]() |
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-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 688 con2bidc 861 con2biddc 866 pm5.17dc 890 bigolden 940 nbbndc 1373 bilukdc 1375 falbitru 1396 3impexpbicom 1415 exists1 2096 eqcom 2142 abeq1 2250 necon2abiddc 2375 necon2bbiddc 2376 necon4bbiddc 2383 ssequn1 3251 axpow3 4109 isocnv 5720 suplocsrlem 7640 uzennn 10240 bezoutlemle 11732 |
Copyright terms: Public domain | W3C validator |