Theorem bibi2i 338

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 287	. 2 ⊢ ((𝜒 ↔ 𝜑) → (𝜒 ↔ 𝜓))
4		id 22	. . 3 ⊢ ((𝜒 ↔ 𝜓) → (𝜒 ↔ 𝜓))
5	4, 2	bitr4di 289	. 2 ⊢ ((𝜒 ↔ 𝜓) → (𝜒 ↔ 𝜑))
6	3, 5	impbii 208	1 ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓))

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