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  694  sbcof2  1834  sblimv  1919  sbhb  1969  sblim  1986  2sb6  2013  sbcom2v  2014  2sb6rf  2019  eu1  2080  moabs  2104  mo3h  2108  moanim  2129  2moswapdc  2145  r2alf  2524  r19.21t  2582  rspc2gv  2893  reu2  2965  reu8  2973  2reuswapdc  2981  2rmorex  2983  dfdif3  3287  ssconb  3310  ssin  3399  reldisj  3516  ssundifim  3548  ralm  3568  unissb  3886  repizf2lem  4213  elirr  4597  en2lp  4610  tfi  4638  ssrel  4771  ssrel2  4773  fncnv  5349  fun11  5350  axcaucvglemres  8032  axpre-suploc  8035  suprzclex  9491  raluz2  9720  supinfneg  9736  infsupneg  9737  infssuzex  10398  bezoutlemmain  12394  isprm2  12514  lmres  14795  ivthdich  15200  limcdifap  15209