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  9350  raluz2  9578  supinfneg  9594  infsupneg  9595  infssuzex  11949  bezoutlemmain  11998  isprm2  12116  lmres  13718  limcdifap  14101