Theorem mp3an23 1314

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 1311	. 2 |- ( ( ph /\ ps ) -> th )
5	1, 4	mpan2 669	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ w3a 971

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 369  df-3an 973

This theorem is referenced by:  sbciegf  3284  ac6sfi  7679  unfilem1  7699  ordtypelem2  7859  infxpenc2  8312  infxpenc2OLD  8316  cda0en  8472  cfsmolem  8563  axdc4lem  8748  1nqenq  9251  mul02lem1  9667  muleqadd  10110  halfcl  10681  rehalfcl  10682  half0  10683  2halves  10684  halfpos2  10685  halfnneg2  10687  halfaddsub  10689  nneo  10863  zeo  10865  peano5uzi  10868  fztp  11658  uzrdgxfr  11980  bcn2  12299  bcpasc  12301  hashxplem  12395  hashfun  12399  swrds2  12794  repsw2  12799  repsw3  12800  imre  12943  reim  12944  crim  12950  addcj  12983  imval2  12986  cnpart  13075  sqrlem7  13084  absmax  13164  efgt0  13840  sinf  13861  efi4p  13874  resin4p  13875  recos4p  13876  sinneg  13883  efival  13889  cosadd  13902  sinmul  13909  sinbnd  13917  cosbnd  13918  ef01bndlem  13921  sin01bnd  13922  cos01bnd  13923  sin01gt0  13927  cos01gt0  13928  sin02gt0  13929  rpnnen2lem11  13960  rpnnen2  13961  odd2np1lem  14047  odd2np1  14048  pythagtriplem12  14352  pythagtriplem14  14354  pythagtriplem15  14355  pythagtriplem16  14356  pythagtriplem17  14357  pockthi  14427  prmreclem5  14440  prmreclem6  14441  prmlem0  14593  prdsplusg  14865  prdsmulr  14866  prdsvsca  14867  odinf  16702  lbsexg  17923  psgnghm2  18708  mopnex  21107  tngnm  21250  tngngp2  21251  tngngpd  21252  tngngp  21253  addccncf  21505  iihalf1  21516  iihalf2  21518  pjthlem1  21937  ovolunlem1a  21992  ovolunlem1  21993  opnmbllem  22095  vitalilem4  22105  iblcnlem1  22279  itgcnlem  22281  dvmptre  22457  dvmptim  22458  dvlipcn  22480  mdegldg  22551  aaliou3lem3  22825  aaliou3lem8  22826  sincosq1lem  22975  sincosq2sgn  22977  sincosq3sgn  22978  sincosq4sgn  22979  sinq12gt0  22985  abssinper  22996  coskpi  22998  sineq0  22999  coseq1  23000  efeq1  23001  resinf1o  23008  efif1olem2  23015  efif1olem4  23017  logneg2  23087  cxpsqrtlem  23170  cxpsqrt  23171  logsqrt  23172  1cubr  23289  leibpilem1  23387  leibpilem2  23388  basellem3  23473  ppiub  23596  chtublem  23603  chtub  23604  bcmax  23670  bcp1ctr  23671  bposlem2  23677  bposlem6  23681  bposlem9  23684  logdivsum  23835  4ipval2  25735  4ipval3  25739  ipidsq  25740  dipcl  25742  dipcj  25744  ipasslem11  25872  hvmul0  26058  pjhthlem1  26426  h1de2bi  26589  spanunsni  26614  adjeu  26924  nmopge0  26946  nmfnge0  26962  opsqrlem6  27180  mdsl1i  27356  mdsl2bi  27358  mdexchi  27370  superpos  27389  atabsi  27436  dmdbr5ati  27457  cdj3lem1  27469  fpwrelmapffslem  27705  ogrpaddlt  27861  ofldlt1  27957  ofldchr  27958  oddpwdc  28476  eulerpartgbij  28494  subfacp1lem2a  28813  subfacp1lem5  28817  subfacp1lem6  28818  subfaclim  28821  sinccvglem  29227  binomfallfaclem2  29328  dfon2lem3  29382  dfon2lem7  29386  predeq1  29411  wrecseq1  29504  wsuceq1  29536  bpoly2  29972  bpoly3  29973  fsumcube  29975  sin2h  30210  cos2h  30211  tan2h  30212  opnmbllem0  30215  mblfinlem3  30218  dvtanlemOLD  30230  itg2addnclem3  30234  ftc1cnnclem  30254  ftc1anclem6  30261  ftc2nc  30265  dvasin  30269  clsun  30312  fdc  30404  constcncf  30421  sub1cncf  30423  sub2cncf  30424  heiborlem7  30479  diophren  30912  lhe4.4ex1a  31402  dirkerper  32044  zlmodzxznm  33298  sinh-conventional  33469  dp2cl  33499  dpfrac1  33502  atlatmstc  35457  dftrcl3  38231  dfrtrcl3  38232  cotrclrcl  38250