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  696  sbcof2  1856  sblimv  1941  sbhb  1991  sblim  2008  2sb6  2035  sbcom2v  2036  2sb6rf  2041  eu1  2102  moabs  2127  mo3h  2131  moanim  2152  2moswapdc  2168  r2alf  2547  r19.21t  2605  rspc2gv  2919  reu2  2991  reu8  2999  2reuswapdc  3007  2rmorex  3009  dfdif3  3314  ssconb  3337  ssin  3426  reldisj  3543  ssundifim  3575  ralm  3595  unissb  3917  repizf2lem  4244  elirr  4632  en2lp  4645  tfi  4673  ssrel  4806  ssrel2  4808  fncnv  5386  fun11  5387  axcaucvglemres  8082  axpre-suploc  8085  suprzclex  9541  raluz2  9770  supinfneg  9786  infsupneg  9787  infssuzex  10448  bezoutlemmain  12514  isprm2  12634  lmres  14916  ivthdich  15321  limcdifap  15330