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  559  xorass  1511  sblbis  2306  sbrbif  2308  abeq2w  2815  abeq2  2872  abeq2f  2940  pm13.183  3597  dfss2  3907  eq0  4277  eq0rdv  4338  disj  4381  disj3  4387  rzal  4439  axrep5  5215  axrep6  5216  axsepgfromrep  5221  ax6vsep  5227  inex1  5241  axprALT  5345  zfpair2  5353  sucel  6339  suppvalbr  7981  bnj89  32700  fineqvrep  33064  axrepprim  33643  brtxpsd3  34198  bisym1  34608  bj-bixor  34773  eliminable-veqab  35050  bj-snsetex  35153  bj-reabeq  35217  wl-3xorbi  35644  sn-axrep5v  40185  ifpidg  41098  nanorxor  41923  mo0sn  46161