Theorem mp3an23 1299

Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)

Hypotheses

Ref	Expression
mp3an23.1	|- ps
mp3an23.2	|- ch
mp3an23.3	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
mp3an23	|- ( ph -> th )

Proof of Theorem mp3an23

Step	Hyp	Ref	Expression
1		mp3an23.1	. 2 |- ps
2		mp3an23.2	. . 3 |- ch
3		mp3an23.3	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
4	2, 3	mp3an3 1296	. 2 |- ( ( ph /\ ps ) -> th )
5	1, 4	mpan2 664	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ w3a 958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 960

This theorem is referenced by:  sbciegf  3206  ac6sfi  7544  unfilem1  7564  ordtypelem2  7721  infxpenc2  8176  infxpenc2OLD  8180  cda0en  8336  cfsmolem  8427  axdc4lem  8612  1nqenq  9119  mul02lem1  9533  muleqadd  9968  halfcl  10538  rehalfcl  10539  half0  10540  2halves  10541  halfpos2  10542  halfnneg2  10544  halfaddsub  10546  nneo  10713  zeo  10715  peano5uzi  10718  fztp  11497  uzrdgxfr  11773  bcn2  12079  bcpasc  12081  hashxplem  12179  hashfun  12183  swrds2  12529  repsw2  12534  repsw3  12535  imre  12581  reim  12582  crim  12588  addcj  12621  imval2  12624  cnpart  12713  sqrlem7  12722  absmax  12801  efgt0  13370  sinf  13391  efi4p  13404  resin4p  13405  recos4p  13406  sinneg  13413  efival  13419  cosadd  13432  sinmul  13439  sinbnd  13447  cosbnd  13448  ef01bndlem  13451  sin01bnd  13452  cos01bnd  13453  sin01gt0  13457  cos01gt0  13458  sin02gt0  13459  rpnnen2lem11  13490  rpnnen2  13491  odd2np1lem  13574  odd2np1  13575  pythagtriplem12  13876  pythagtriplem14  13878  pythagtriplem15  13879  pythagtriplem16  13880  pythagtriplem17  13881  pockthi  13951  prmreclem5  13964  prmreclem6  13965  prmlem0  14116  prdsplusg  14379  prdsmulr  14380  prdsvsca  14381  odinf  16044  lbsexg  17167  psgnghm2  17853  mopnex  19936  tngnm  20079  tngngp2  20080  tngngpd  20081  tngngp  20082  addccncf  20334  iihalf1  20345  iihalf2  20347  pjthlem1  20766  ovolunlem1a  20821  ovolunlem1  20822  opnmbllem  20923  vitalilem4  20933  iblcnlem1  21107  itgcnlem  21109  dvmptre  21285  dvmptim  21286  dvlipcn  21308  mdegldg  21422  aaliou3lem3  21695  aaliou3lem8  21696  sincosq1lem  21844  sincosq2sgn  21846  sincosq3sgn  21847  sincosq4sgn  21848  sinq12gt0  21854  abssinper  21865  coskpi  21867  sineq0  21868  coseq1  21869  efeq1  21870  resinf1o  21877  efif1olem2  21884  efif1olem4  21886  logneg2  21949  cxpsqrlem  22032  cxpsqr  22033  logsqr  22034  1cubr  22122  leibpilem1  22220  leibpilem2  22221  basellem3  22305  ppiub  22428  chtublem  22435  chtub  22436  bcmax  22502  bcp1ctr  22503  bposlem2  22509  bposlem6  22513  bposlem9  22516  logdivsum  22667  4ipval2  23926  4ipval3  23930  ipidsq  23931  dipcl  23933  dipcj  23935  ipasslem11  24063  hvmul0  24249  pjhthlem1  24617  h1de2bi  24780  spanunsni  24805  adjeu  25116  nmopge0  25138  nmfnge0  25154  opsqrlem6  25372  mdsl1i  25548  mdsl2bi  25550  mdexchi  25562  superpos  25581  atabsi  25628  dmdbr5ati  25649  cdj3lem1  25661  ogrpaddlt  26005  ofldlt1  26134  ofldchr  26135  oddpwdc  26585  subfacp1lem2a  26916  subfacp1lem5  26920  subfacp1lem6  26921  subfaclim  26924  sinccvglem  27164  binomfallfaclem2  27390  dfon2lem3  27445  dfon2lem7  27449  predeq1  27474  wrecseq1  27567  wsuceq1  27599  bpoly2  28047  bpoly3  28048  fsumcube  28050  sin2h  28266  cos2h  28267  tan2h  28268  opnmbllem0  28271  mblfinlem3  28274  dvtanlem  28285  itg2addnclem3  28289  ftc1cnnclem  28309  ftc1anclem6  28316  ftc2nc  28320  dvasin  28324  clsun  28367  fdc  28485  constcncf  28502  sub1cncf  28504  sub2cncf  28505  heiborlem7  28560  diophren  28997  lhe4.4ex1a  29448  zlmodzxznm  30769  sinh-conventional  30804  dp2cl  30834  dpfrac1  30837  atlatmstc  32558