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  4205  elirr  4589  en2lp  4602  tfi  4630  ssrel  4763  ssrel2  4765  fncnv  5340  fun11  5341  axcaucvglemres  8012  axpre-suploc  8015  suprzclex  9471  raluz2  9700  supinfneg  9716  infsupneg  9717  infssuzex  10376  bezoutlemmain  12319  isprm2  12439  lmres  14720  ivthdich  15125  limcdifap  15134