![]() |
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 | bitrdi 287 | . 2 ⊢ ((𝜒 ↔ 𝜑) → (𝜒 ↔ 𝜓)) |
4 | id 22 | . . 3 ⊢ ((𝜒 ↔ 𝜓) → (𝜒 ↔ 𝜓)) | |
5 | 4, 2 | bitr4di 289 | . 2 ⊢ ((𝜒 ↔ 𝜓) → (𝜒 ↔ 𝜑)) |
6 | 3, 5 | impbii 208 | 1 ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 |
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 206 |
This theorem is referenced by: bibi1i 339 bibi12i 340 bibi2d 343 con2bi 354 pm4.71r 560 xorass 1515 sblbis 2306 sbrbif 2308 eqabbw 2810 eqabbOLD 2875 eqabf 2936 pm13.183 3654 dfss2 3966 eq0 4341 eq0rdv 4402 disj 4445 disj3 4451 rzal 4504 axrep5 5287 axrep6 5288 axsepgfromrep 5293 ax6vsep 5299 inex1 5313 axprALT 5416 zfpair2 5424 sucel 6430 suppvalbr 8137 bnj89 33663 fineqvrep 34026 axrepprim 34602 brtxpsd3 34799 bisym1 35209 bj-bixor 35374 eliminable-veqab 35650 bj-snsetex 35749 bj-reabeq 35813 bj-clex 35817 wl-3xorbi 36259 sn-axrep5v 40949 ifpidg 42113 nanorxor 42935 mo0sn 47340 |
Copyright terms: Public domain | W3C validator |