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 211 | . 2 ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜒 ↔ 𝜑)) | |
2 | bibi2i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
3 | 2 | bibi2i 326 | . 2 ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓)) |
4 | bicom 211 | . 2 ⊢ ((𝜒 ↔ 𝜓) ↔ (𝜓 ↔ 𝜒)) | |
5 | 1, 3, 4 | 3bitri 285 | 1 ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 |
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 196 |
This theorem is referenced by: bibi12i 328 biluk 970 xorass 1460 hadbi 1528 hadnot 1532 sbrbis 2393 ssequn1 3745 symdifass 3815 asymref 5431 aceq1 8823 aceq0 8824 zfac 9165 zfcndac 9320 funcnvmptOLD 28850 axacprim 30838 rp-fakeanorass 36877 rp-fakenanass 36879 |
Copyright terms: Public domain | W3C validator |