Theorem imbi2i 224

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

Syntax hints:   → wi 4   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  imbi12i  237  anidmdbi  390  nan  658  sbcof2  1731  sblimv  1815  sbhb  1857  sblim  1872  2sb6  1901  sbcom2v  1902  2sb6rf  1907  eu1  1966  moabs  1990  mo3h  1994  moanim  2015  2moswapdc  2031  r2alf  2383  r19.21t  2436  rspc2gv  2712  reu2  2780  reu8  2788  2reuswapdc  2794  2rmorex  2796  ssconb  3105  ssin  3188  reldisj  3295  ssundifim  3326  ralm  3345  unissb  3631  repizf2lem  3935  elirr  4284  en2lp  4297  tfi  4323  ssrel  4446  ssrel2  4448  fncnv  4985  fun11  4986  axcaucvglemres  7065  suprzclex  8445  raluz2  8667  supinfneg  8683  infsupneg  8684  infssuzex  10345  bezoutlemmain  10387  isprm2  10499