Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > bibi1i | Structured version Visualization version GIF version |
Description: Inference adding a biconditional to the right in an equivalence. (Contributed by NM, 26-May-1993.) |
Ref | Expression |
---|---|
bibi2i.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
bibi1i | ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bicom 224 | . 2 ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜒 ↔ 𝜑)) | |
2 | bibi2i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
3 | 2 | bibi2i 340 | . 2 ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓)) |
4 | bicom 224 | . 2 ⊢ ((𝜒 ↔ 𝜓) ↔ (𝜓 ↔ 𝜒)) | |
5 | 1, 3, 4 | 3bitri 299 | 1 ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 |
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 209 |
This theorem is referenced by: bibi12i 342 biluk 389 biadaniALT 819 nanass 1500 xorass 1506 hadbi 1598 hadcoma 1599 hadnot 1603 sbrbis 2320 ssequn1 4158 asymref 5978 aceq1 9545 aceq0 9546 zfac 9884 zfcndac 10043 hashreprin 31893 axacprim 32935 redundpbi1 35868 rp-fakeanorass 39886 dfich2 43620 dfich2ai 43621 ichn 43633 |
Copyright terms: Public domain | W3C validator |