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  2853  reu2  2925  reu8  2933  2reuswapdc  2941  2rmorex  2943  dfdif3  3245  ssconb  3268  ssin  3357  reldisj  3474  ssundifim  3506  ralm  3527  unissb  3839  repizf2lem  4161  elirr  4540  en2lp  4553  tfi  4581  ssrel  4714  ssrel2  4716  fncnv  5282  fun11  5283  axcaucvglemres  7897  axpre-suploc  7900  suprzclex  9349  raluz2  9577  supinfneg  9593  infsupneg  9594  infssuzex  11944  bezoutlemmain  11993  isprm2  12111  lmres  13641  limcdifap  14024