Theorem bibi2i 337

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 209	1 ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓))

Syntax hints:   ↔ wb 206

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 207

This theorem is referenced by:  bibi1i  338  bibi12i  339  bibi2d  342  con2bi  353  pm4.71r  558  xorass  1515  sblbis  2308  sbrbif  2310  eqabbw  2803  eqabbOLD  2869  eqabf  2922  eq0  4316  eq0rdv  4373  disj  4416  disj3  4420  rzal  4475  axrep4v  5242  axrep4  5243  axrep5  5245  axrep6  5246  axrep6OLD  5247  axsepgfromrep  5252  ax6vsep  5261  inex1  5275  axprALT  5380  zfpair2  5391  sucel  6411  suppvalbr  8146  bnj89  34718  fineqvrep  35092  axrepprim  35696  brtxpsd3  35891  bisym1  36414  bj-bixor  36586  eliminable-veqab  36861  bj-snsetex  36958  bj-reabeq  37022  bj-clex  37026  wl-3xorbi  37468  sn-axrep5v  42211  ifpidg  43487  nanorxor  44301  mo0sn  48808