Theorem mp3an23 1416

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

Syntax hints:   -> wi 4   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  sbciegf  3467  predeq1  5682  wrecseq1  7410  ac6sfi  8204  unfilem1  8224  ordtypelem2  8424  infxpenc2  8845  cda0en  9001  cfsmolem  9092  axdc4lem  9277  1nqenq  9784  mul02lem1  10212  muleqadd  10671  halfcl  11257  rehalfcl  11258  half0  11259  2halves  11260  halfpos2  11261  halfnneg2  11263  halfaddsub  11265  nneo  11461  zeo  11463  peano5uzi  11466  fztp  12397  uzrdgxfr  12766  bcn2  13106  bcpasc  13108  hashxplem  13220  hashfun  13224  swrds2  13685  repsw2  13693  repsw3  13694  imre  13848  reim  13849  crim  13855  addcj  13888  imval2  13891  cnpart  13980  sqrlem7  13989  absmax  14069  binomfallfaclem2  14771  bpoly2  14788  bpoly3  14789  fsumcube  14791  efgt0  14833  sinf  14854  efi4p  14867  resin4p  14868  recos4p  14869  sinneg  14876  efival  14882  cosadd  14895  sinmul  14902  sinbnd  14910  cosbnd  14911  ef01bndlem  14914  sin01bnd  14915  cos01bnd  14916  sin01gt0  14920  cos01gt0  14921  sin02gt0  14922  rpnnen2lem11  14953  rpnnen2lem12  14954  odd2np1lem  15064  odd2np1  15065  pythagtriplem12  15531  pythagtriplem14  15533  pythagtriplem15  15534  pythagtriplem16  15535  pythagtriplem17  15536  pockthi  15611  prmreclem5  15624  prmreclem6  15625  prmlem0  15812  prdsplusg  16118  prdsmulr  16119  prdsvsca  16120  odinf  17980  lbsexg  19164  psgnghm2  19927  mopnex  22324  tngnm  22455  tngngp2  22456  tngngpd  22457  tngngp  22458  addccncf  22719  iihalf1  22730  iihalf2  22732  pjthlem1  23208  ovolunlem1a  23264  ovolunlem1  23265  opnmbllem  23369  vitalilem4  23380  iblcnlem1  23554  itgcnlem  23556  dvmptre  23732  dvmptim  23733  dvlipcn  23757  mdegldg  23826  aaliou3lem3  24099  aaliou3lem8  24100  sincosq1lem  24249  sincosq2sgn  24251  sincosq3sgn  24252  sincosq4sgn  24253  sinq12gt0  24259  abssinper  24270  coskpi  24272  sineq0  24273  coseq1  24274  efeq1  24275  resinf1o  24282  efif1olem2  24289  efif1olem4  24291  logneg2  24361  cxpsqrtlem  24448  cxpsqrt  24449  logsqrt  24450  1cubr  24569  leibpilem1  24667  leibpilem2  24668  basellem3  24809  ppiub  24929  chtublem  24936  chtub  24937  bcmax  25003  bcp1ctr  25004  bposlem2  25010  bposlem6  25014  bposlem9  25017  logdivsum  25222  4ipval2  27563  ipidsq  27565  dipcl  27567  dipcj  27569  ipasslem11  27695  hvmul0  27881  pjhthlem1  28250  h1de2bi  28413  spanunsni  28438  adjeu  28748  nmopge0  28770  nmfnge0  28786  opsqrlem6  29004  mdsl1i  29180  mdsl2bi  29182  mdexchi  29194  superpos  29213  atabsi  29260  dmdbr5ati  29281  cdj3lem1  29293  fpwrelmapffslem  29507  dp2cl  29587  dpfrac1  29599  dpfrac1OLD  29600  ogrpaddlt  29718  ofldlt1  29813  ofldchr  29814  oddpwdc  30416  eulerpartgbij  30434  subfacp1lem2a  31162  subfacp1lem5  31166  subfacp1lem6  31167  subfaclim  31170  sinccvglem  31566  dfon2lem3  31690  dfon2lem7  31694  wsuceq1  31761  clsun  32323  vtoclefex  33181  finxpreclem5  33232  sin2h  33399  cos2h  33400  tan2h  33401  poimirlem22  33431  poimirlem31  33440  opnmbllem0  33445  mblfinlem3  33448  itg2addnclem3  33463  ftc1cnnclem  33483  ftc1anclem6  33490  ftc2nc  33494  dvasin  33496  fdc  33541  constcncf  33558  sub1cncf  33560  sub2cncf  33561  heiborlem7  33616  atlatmstc  34606  diophren  37377  dftrcl3  38012  dfrtrcl3  38025  cotrclrcl  38034  lhe4.4ex1a  38528  dirkerper  40313  zlmodzxznm  42286  sinh-conventional  42480