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 4156 asymref 5976 aceq1 9543 aceq0 9544 zfac 9882 zfcndac 10041 hashreprin 31891 axacprim 32933 wl-hadcoma 34755 wl-hadnot 34757 redundpbi1 35881 rp-fakeanorass 39899 dfich2 43633 dfich2ai 43634 ichn 43646 |
Copyright terms: Public domain | W3C validator |