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  699  sbcof2  1859  sblimv  1946  sbhb  1996  sblim  2013  2sb6  2040  sbcom2v  2041  2sb6rf  2046  eu1  2107  moabs  2132  mo3h  2136  moanim  2157  2moswapdc  2173  r2alf  2561  r19.21t  2619  rspc2gv  2936  reu2  3008  reu8  3016  2reuswapdc  3024  2rmorex  3026  dfdif3  3333  ssconb  3356  ssin  3447  reldisj  3564  ssundifim  3597  ralm  3617  unissb  3949  repizf2lem  4279  elirr  4668  en2lp  4681  tfi  4709  ssrel  4843  ssrel2  4845  fncnv  5427  fun11  5428  axcaucvglemres  8230  axpre-suploc  8233  suprzclex  9694  raluz2  9929  supinfneg  9945  infsupneg  9946  infssuzex  10615  bezoutlemmain  12719  isprm2  12839  lmres  15239  ivthdich  15644  limcdifap  15653