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  1832  sblimv  1917  sbhb  1967  sblim  1984  2sb6  2011  sbcom2v  2012  2sb6rf  2017  eu1  2078  moabs  2102  mo3h  2106  moanim  2127  2moswapdc  2143  r2alf  2522  r19.21t  2580  rspc2gv  2888  reu2  2960  reu8  2968  2reuswapdc  2976  2rmorex  2978  dfdif3  3282  ssconb  3305  ssin  3394  reldisj  3511  ssundifim  3543  ralm  3563  unissb  3879  repizf2lem  4204  elirr  4588  en2lp  4601  tfi  4629  ssrel  4762  ssrel2  4764  fncnv  5339  fun11  5340  axcaucvglemres  8011  axpre-suploc  8014  suprzclex  9470  raluz2  9699  supinfneg  9715  infsupneg  9716  infssuzex  10374  bezoutlemmain  12261  isprm2  12381  lmres  14662  ivthdich  15067  limcdifap  15076