![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > bibi2i | Structured version Visualization version GIF version |
Description: Inference adding a biconditional to the left in an equivalence. (Contributed by NM, 26-May-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 16-May-2013.) |
Ref | Expression |
---|---|
bibi2i.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
bibi2i | ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . . 3 ⊢ ((𝜒 ↔ 𝜑) → (𝜒 ↔ 𝜑)) | |
2 | bibi2i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
3 | 1, 2 | syl6bb 276 | . 2 ⊢ ((𝜒 ↔ 𝜑) → (𝜒 ↔ 𝜓)) |
4 | id 22 | . . 3 ⊢ ((𝜒 ↔ 𝜓) → (𝜒 ↔ 𝜓)) | |
5 | 4, 2 | syl6bbr 278 | . 2 ⊢ ((𝜒 ↔ 𝜓) → (𝜒 ↔ 𝜑)) |
6 | 3, 5 | impbii 199 | 1 ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 |
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 197 |
This theorem is referenced by: bibi1i 327 bibi12i 328 bibi2d 331 con2bi 342 pm4.71r 666 xorass 1617 sblbis 2542 sbrbif 2544 abeq2 2871 abeq2f 2931 pm13.183 3485 symdifass 3997 disj3 4165 euabsn2 4405 axrep5 4929 axsep 4933 ax6vsep 4938 inex1 4952 axpr 5055 zfpair2 5057 sucel 5960 suppvalbr 7469 bnj89 31118 axrepprim 31908 brtxpsd3 32331 bisym1 32746 bj-abeq2 33102 bj-axrep5 33121 bj-axsep 33122 bj-snsetex 33276 ifpidg 38357 nanorxor 39025 |
Copyright terms: Public domain | W3C validator |