Theorem imbi2i 224

Description: Introduce an antecedent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 6-Feb-2013.)

Hypothesis

Ref	Expression
bi.a	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
imbi2i	⊢ ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))

Proof of Theorem imbi2i

Step	Hyp	Ref	Expression
1		bi.a	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 9	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜓))
3	2	pm5.74i 178	1 ⊢ ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  imbi12i  237  anidmdbi  390  nan  661  sbcof2  1738  sblimv  1822  sbhb  1864  sblim  1879  2sb6  1908  sbcom2v  1909  2sb6rf  1914  eu1  1973  moabs  1997  mo3h  2001  moanim  2022  2moswapdc  2038  r2alf  2395  r19.21t  2448  rspc2gv  2733  reu2  2803  reu8  2811  2reuswapdc  2819  2rmorex  2821  dfdif3  3110  ssconb  3133  ssin  3222  reldisj  3334  ssundifim  3366  ralm  3386  unissb  3683  repizf2lem  3996  elirr  4357  en2lp  4370  tfi  4397  ssrel  4526  ssrel2  4528  fncnv  5080  fun11  5081  axcaucvglemres  7432  suprzclex  8842  raluz2  9065  supinfneg  9081  infsupneg  9082  infssuzex  11219  bezoutlemmain  11261  isprm2  11373