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  694  sbcof2  1834  sblimv  1919  sbhb  1969  sblim  1986  2sb6  2013  sbcom2v  2014  2sb6rf  2019  eu1  2080  moabs  2105  mo3h  2109  moanim  2130  2moswapdc  2146  r2alf  2525  r19.21t  2583  rspc2gv  2896  reu2  2968  reu8  2976  2reuswapdc  2984  2rmorex  2986  dfdif3  3291  ssconb  3314  ssin  3403  reldisj  3520  ssundifim  3552  ralm  3572  unissb  3894  repizf2lem  4221  elirr  4607  en2lp  4620  tfi  4648  ssrel  4781  ssrel2  4783  fncnv  5359  fun11  5360  axcaucvglemres  8047  axpre-suploc  8050  suprzclex  9506  raluz2  9735  supinfneg  9751  infsupneg  9752  infssuzex  10413  bezoutlemmain  12434  isprm2  12554  lmres  14835  ivthdich  15240  limcdifap  15249