| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > bicom | Structured version Visualization version GIF version | ||
| Description: Commutative law for the biconditional. Theorem *4.21 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-1993.) |
| Ref | Expression |
|---|---|
| bicom | ⊢ ((𝜑 ↔ 𝜓) ↔ (𝜓 ↔ 𝜑)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bicom1 221 | . 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑)) | |
| 2 | bicom1 221 | . 2 ⊢ ((𝜓 ↔ 𝜑) → (𝜑 ↔ 𝜓)) | |
| 3 | 1, 2 | impbii 209 | 1 ⊢ ((𝜑 ↔ 𝜓) ↔ (𝜓 ↔ 𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This theorem depends on definitions: df-bi 207 |
| This theorem is referenced by: bicomd 223 bibi1i 338 bibi1d 343 con2bi 353 ibibr 368 bibif 371 nbbn 383 biluk 385 biadan 819 pm5.17 1014 bigolden 1029 xorcom 1514 norass 1537 trubifal 1571 hadcoma 1599 eqabcb 2883 pm13.183 3666 ssequn1 4186 ab0w 4379 disj 4450 isocnv 7350 qextlt 13245 qextle 13246 rpnnen2lem12 16261 odd2np1 16378 sumodd 16425 nrmmetd 24587 lgsqrmodndvds 27397 eqelbid 32494 mgccnv 32989 cvmlift2lem12 35319 nn0prpw 36324 wl-3xorrot 37478 wl-3xorcoma 37479 tsbi4 38143 bicomdd 38855 onsupmaxb 43251 ifpbicor 43488 rp-fakeoranass 43527 or3or 44036 3impexpbicom 44500 3impexpbicomVD 44877 notbicom 45170 limsupreuz 45752 nabctnabc 46943 |
| Copyright terms: Public domain | W3C validator |