Theorem imbi2i 225

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 179	1 ⊢ ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  imbi12i  238  anidmdbi  395  nan  681  sbcof2  1782  sblimv  1866  sbhb  1913  sblim  1930  2sb6  1959  sbcom2v  1960  2sb6rf  1965  eu1  2024  moabs  2048  mo3h  2052  moanim  2073  2moswapdc  2089  r2alf  2452  r19.21t  2507  rspc2gv  2801  reu2  2872  reu8  2880  2reuswapdc  2888  2rmorex  2890  dfdif3  3186  ssconb  3209  ssin  3298  reldisj  3414  ssundifim  3446  ralm  3467  unissb  3766  repizf2lem  4085  elirr  4456  en2lp  4469  tfi  4496  ssrel  4627  ssrel2  4629  fncnv  5189  fun11  5190  axcaucvglemres  7707  axpre-suploc  7710  suprzclex  9149  raluz2  9374  supinfneg  9390  infsupneg  9391  infssuzex  11642  bezoutlemmain  11686  isprm2  11798  lmres  12417  limcdifap  12800