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	|- ( ph <-> ps )

Assertion

Ref	Expression
imbi2i	|- ( ( ch -> ph ) <-> ( ch -> ps ) )

Proof of Theorem imbi2i

Step	Hyp	Ref	Expression
1		bi.a	. . 3 |- ( ph <-> ps )
2	1	a1i 9	. 2 |- ( ch -> ( ph <-> ps ) )
3	2	pm5.74i 180	1 |- ( ( ch -> ph ) <-> ( ch -> ps ) )

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  692  sbcof2  1810  sblimv  1894  sbhb  1940  sblim  1957  2sb6  1984  sbcom2v  1985  2sb6rf  1990  eu1  2051  moabs  2075  mo3h  2079  moanim  2100  2moswapdc  2116  r2alf  2494  r19.21t  2552  rspc2gv  2855  reu2  2927  reu8  2935  2reuswapdc  2943  2rmorex  2945  dfdif3  3247  ssconb  3270  ssin  3359  reldisj  3476  ssundifim  3508  ralm  3529  unissb  3841  repizf2lem  4163  elirr  4542  en2lp  4555  tfi  4583  ssrel  4716  ssrel2  4718  fncnv  5284  fun11  5285  axcaucvglemres  7900  axpre-suploc  7903  suprzclex  9353  raluz2  9581  supinfneg  9597  infsupneg  9598  infssuzex  11952  bezoutlemmain  12001  isprm2  12119  lmres  13787  limcdifap  14170