Theorem imbi2i 225

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

Syntax hints:   → wi 4   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  imbi12i  238  anidmdbi  396  nan  682  sbcof2  1790  sblimv  1874  sbhb  1920  sblim  1937  2sb6  1964  sbcom2v  1965  2sb6rf  1970  eu1  2031  moabs  2055  mo3h  2059  moanim  2080  2moswapdc  2096  r2alf  2474  r19.21t  2532  rspc2gv  2828  reu2  2900  reu8  2908  2reuswapdc  2916  2rmorex  2918  dfdif3  3217  ssconb  3240  ssin  3329  reldisj  3445  ssundifim  3477  ralm  3498  unissb  3803  repizf2lem  4123  elirr  4501  en2lp  4514  tfi  4542  ssrel  4675  ssrel2  4677  fncnv  5237  fun11  5238  axcaucvglemres  7820  axpre-suploc  7823  suprzclex  9263  raluz2  9491  supinfneg  9507  infsupneg  9508  infssuzex  11840  bezoutlemmain  11886  isprm2  11998  lmres  12690  limcdifap  13073