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  4587  en2lp  4600  tfi  4628  ssrel  4761  ssrel2  4763  fncnv  5334  fun11  5335  axcaucvglemres  7994  axpre-suploc  7997  suprzclex  9453  raluz2  9682  supinfneg  9698  infsupneg  9699  infssuzex  10357  bezoutlemmain  12238  isprm2  12358  lmres  14638  ivthdich  15043  limcdifap  15052