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 222 | . 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑)) | |
2 | bicom1 222 | . 2 ⊢ ((𝜓 ↔ 𝜑) → (𝜑 ↔ 𝜓)) | |
3 | 1, 2 | impbii 210 | 1 ⊢ ((𝜑 ↔ 𝜓) ↔ (𝜓 ↔ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 |
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 208 |
This theorem is referenced by: bicomd 224 bibi1i 340 bibi1d 345 con2bi 355 ibibr 370 bibif 373 nbbn 385 biluk 387 biadan 815 pm5.17 1005 bigolden 1020 xorcom 1498 norass 1524 trubifal 1559 hadcoma 1590 abeq1 2946 ssequn1 4155 axpow3 5261 isocnv 7072 qextlt 12586 qextle 12587 rpnnen2lem12 15568 odd2np1 15680 sumodd 15729 nrmmetd 23113 lgsqrmodndvds 25857 cvmlift2lem12 32459 nn0prpw 33569 tsbi4 35297 bicomdd 35872 ifpbicor 39721 rp-fakeoranass 39760 or3or 40251 3impexpbicom 40693 3impexpbicomVD 41071 limsupreuz 41898 nabctnabc 43048 isomuspgrlem2b 43841 |
Copyright terms: Public domain | W3C validator |