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  1833  sblimv  1918  sbhb  1968  sblim  1985  2sb6  2012  sbcom2v  2013  2sb6rf  2018  eu1  2079  moabs  2103  mo3h  2107  moanim  2128  2moswapdc  2144  r2alf  2523  r19.21t  2581  rspc2gv  2889  reu2  2961  reu8  2969  2reuswapdc  2977  2rmorex  2979  dfdif3  3283  ssconb  3306  ssin  3395  reldisj  3512  ssundifim  3544  ralm  3564  unissb  3880  repizf2lem  4206  elirr  4590  en2lp  4603  tfi  4631  ssrel  4764  ssrel2  4766  fncnv  5341  fun11  5342  axcaucvglemres  8014  axpre-suploc  8017  suprzclex  9473  raluz2  9702  supinfneg  9718  infsupneg  9719  infssuzex  10378  bezoutlemmain  12352  isprm2  12472  lmres  14753  ivthdich  15158  limcdifap  15167