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  696  sbcof2  1856  sblimv  1941  sbhb  1991  sblim  2008  2sb6  2035  sbcom2v  2036  2sb6rf  2041  eu1  2102  moabs  2127  mo3h  2131  moanim  2152  2moswapdc  2168  r2alf  2547  r19.21t  2605  rspc2gv  2920  reu2  2992  reu8  3000  2reuswapdc  3008  2rmorex  3010  dfdif3  3315  ssconb  3338  ssin  3427  reldisj  3544  ssundifim  3576  ralm  3596  unissb  3921  repizf2lem  4249  elirr  4637  en2lp  4650  tfi  4678  ssrel  4812  ssrel2  4814  fncnv  5393  fun11  5394  axcaucvglemres  8109  axpre-suploc  8112  suprzclex  9568  raluz2  9803  supinfneg  9819  infsupneg  9820  infssuzex  10483  bezoutlemmain  12559  isprm2  12679  lmres  14962  ivthdich  15367  limcdifap  15376