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  1858  sblimv  1943  sbhb  1993  sblim  2010  2sb6  2037  sbcom2v  2038  2sb6rf  2043  eu1  2104  moabs  2129  mo3h  2133  moanim  2154  2moswapdc  2170  r2alf  2550  r19.21t  2608  rspc2gv  2923  reu2  2995  reu8  3003  2reuswapdc  3011  2rmorex  3013  dfdif3  3319  ssconb  3342  ssin  3431  reldisj  3548  ssundifim  3580  ralm  3600  unissb  3928  repizf2lem  4257  elirr  4645  en2lp  4658  tfi  4686  ssrel  4820  ssrel2  4822  fncnv  5403  fun11  5404  axcaucvglemres  8162  axpre-suploc  8165  suprzclex  9622  raluz2  9857  supinfneg  9873  infsupneg  9874  infssuzex  10539  bezoutlemmain  12632  isprm2  12752  lmres  15042  ivthdich  15447  limcdifap  15456