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 290 | . 2 ⊢ ((𝜒 ↔ 𝜑) → (𝜒 ↔ 𝜓)) |
4 | id 22 | . . 3 ⊢ ((𝜒 ↔ 𝜓) → (𝜒 ↔ 𝜓)) | |
5 | 4, 2 | bitr4di 292 | . 2 ⊢ ((𝜒 ↔ 𝜓) → (𝜒 ↔ 𝜑)) |
6 | 3, 5 | impbii 212 | 1 ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 |
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 210 |
This theorem is referenced by: bibi1i 342 bibi12i 343 bibi2d 346 con2bi 357 pm4.71r 562 xorass 1512 sblbis 2310 sbrbif 2312 abeq2w 2815 abeq2 2869 abeq2f 2937 pm13.183 3575 dfss2 3886 eq0 4258 eq0rdv 4319 disj 4362 disj3 4368 rzal 4420 axrep5 5185 axrep6 5186 axsepgfromrep 5190 ax6vsep 5196 inex1 5210 axprALT 5315 zfpair2 5323 sucel 6286 suppvalbr 7907 bnj89 32412 fineqvrep 32777 axrepprim 33356 brtxpsd3 33935 bisym1 34345 bj-bixor 34510 eliminable-veqab 34787 bj-snsetex 34890 bj-reabeq 34954 wl-3xorbi 35381 sn-axrep5v 39907 ifpidg 40783 nanorxor 41596 mo0sn 45834 |
Copyright terms: Public domain | W3C validator |