Theorem imbi2i 226

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

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imbi12i  239  anidmdbi  398  nan  693  sbcof2  1824  sblimv  1909  sbhb  1959  sblim  1976  2sb6  2003  sbcom2v  2004  2sb6rf  2009  eu1  2070  moabs  2094  mo3h  2098  moanim  2119  2moswapdc  2135  r2alf  2514  r19.21t  2572  rspc2gv  2880  reu2  2952  reu8  2960  2reuswapdc  2968  2rmorex  2970  dfdif3  3274  ssconb  3297  ssin  3386  reldisj  3503  ssundifim  3535  ralm  3555  unissb  3870  repizf2lem  4195  elirr  4578  en2lp  4591  tfi  4619  ssrel  4752  ssrel2  4754  fncnv  5325  fun11  5326  axcaucvglemres  7983  axpre-suploc  7986  suprzclex  9441  raluz2  9670  supinfneg  9686  infsupneg  9687  infssuzex  10340  bezoutlemmain  12190  isprm2  12310  lmres  14568  ivthdich  14973  limcdifap  14982