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  1944  sbhb  1994  sblim  2011  2sb6  2038  sbcom2v  2039  2sb6rf  2044  eu1  2105  moabs  2130  mo3h  2134  moanim  2155  2moswapdc  2171  r2alf  2559  r19.21t  2617  rspc2gv  2933  reu2  3005  reu8  3013  2reuswapdc  3021  2rmorex  3023  dfdif3  3329  ssconb  3352  ssin  3443  reldisj  3560  ssundifim  3593  ralm  3613  unissb  3944  repizf2lem  4274  elirr  4663  en2lp  4676  tfi  4704  ssrel  4838  ssrel2  4840  fncnv  5422  fun11  5423  axcaucvglemres  8214  axpre-suploc  8217  suprzclex  9676  raluz2  9911  supinfneg  9927  infsupneg  9928  infssuzex  10593  bezoutlemmain  12694  isprm2  12814  lmres  15113  ivthdich  15518  limcdifap  15527