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  1512  sblbis  2313  sbrbif  2315  eqabbw  2818  eqabbOLD  2885  eqabf  2941  eq0  4373  eq0rdv  4430  disj  4473  disj3  4477  rzal  4532  axrep5  5309  axrep6  5310  axsepgfromrep  5315  ax6vsep  5321  inex1  5335  axprALT  5440  zfpair2  5448  sucel  6469  suppvalbr  8205  bnj89  34697  fineqvrep  35071  axrepprim  35664  brtxpsd3  35860  bisym1  36385  bj-bixor  36557  eliminable-veqab  36832  bj-snsetex  36929  bj-reabeq  36993  bj-clex  36997  wl-3xorbi  37439  sn-axrep5v  42209  ifpidg  43453  nanorxor  44274  mo0sn  48547