Theorem bibi2i 339

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

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  bibi1i  340  bibi12i  341  bibi2d  344  con2bi  355  pm4.71r  566  xorass  1534  sblbis  2341  sbrbif  2343  eqabbw  2834  eqabf  2952  ab0w  4331  disj3  4407  axrep4v  5231  axrep4  5232  axrep5  5234  axrep6  5235  axrep6OLD  5236  zfrep6  5238  axsepgfromrep  5243  ax6vsep  5252  inex1  5272  axprALT  5378  zfpair2  5390  prex  5394  sucel  6418  tz6.12-2  6850  suppvalbr  8139  bnj89  34981  fineqvrep  35374  axrepprim  36016  brtxpsd3  36208  bisym1  36743  mh-infprim3bi  36872  bj-bixor  36998  eliminable-veqab  37315  bj-snsetex  37412  bj-reabeq  37476  bj-clex  37480  bj-rep  37522  bj-axseprep  37523  wl-3xorbi  37931  sn-axrep5v  42800  ifpidg  44031  nanorxor  44845  mo0sn  49401