Theorem bibi2i 341

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.)

Hypothesis

Ref	Expression
bibi2i.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
bibi2i	⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓))

Proof of Theorem 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 ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓))

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