Theorem mp3an23 1316

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

Syntax hints:   -> wi 4   /\ w3a 973

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 975

This theorem is referenced by:  sbciegf  3363  ac6sfi  7764  unfilem1  7784  ordtypelem2  7944  infxpenc2  8399  infxpenc2OLD  8403  cda0en  8559  cfsmolem  8650  axdc4lem  8835  1nqenq  9340  mul02lem1  9755  muleqadd  10193  halfcl  10764  rehalfcl  10765  half0  10766  2halves  10767  halfpos2  10768  halfnneg2  10770  halfaddsub  10772  nneo  10944  zeo  10946  peano5uzi  10949  fztp  11736  uzrdgxfr  12045  bcn2  12365  bcpasc  12367  hashxplem  12457  hashfun  12461  swrds2  12846  repsw2  12851  repsw3  12852  imre  12904  reim  12905  crim  12911  addcj  12944  imval2  12947  cnpart  13036  sqrlem7  13045  absmax  13125  efgt0  13699  sinf  13720  efi4p  13733  resin4p  13734  recos4p  13735  sinneg  13742  efival  13748  cosadd  13761  sinmul  13768  sinbnd  13776  cosbnd  13777  ef01bndlem  13780  sin01bnd  13781  cos01bnd  13782  sin01gt0  13786  cos01gt0  13787  sin02gt0  13788  rpnnen2lem11  13819  rpnnen2  13820  odd2np1lem  13904  odd2np1  13905  pythagtriplem12  14209  pythagtriplem14  14211  pythagtriplem15  14212  pythagtriplem16  14213  pythagtriplem17  14214  pockthi  14284  prmreclem5  14297  prmreclem6  14298  prmlem0  14449  prdsplusg  14713  prdsmulr  14714  prdsvsca  14715  odinf  16391  lbsexg  17610  psgnghm2  18412  mopnex  20785  tngnm  20928  tngngp2  20929  tngngpd  20930  tngngp  20931  addccncf  21183  iihalf1  21194  iihalf2  21196  pjthlem1  21615  ovolunlem1a  21670  ovolunlem1  21671  opnmbllem  21773  vitalilem4  21783  iblcnlem1  21957  itgcnlem  21959  dvmptre  22135  dvmptim  22136  dvlipcn  22158  mdegldg  22229  aaliou3lem3  22502  aaliou3lem8  22503  sincosq1lem  22651  sincosq2sgn  22653  sincosq3sgn  22654  sincosq4sgn  22655  sinq12gt0  22661  abssinper  22672  coskpi  22674  sineq0  22675  coseq1  22676  efeq1  22677  resinf1o  22684  efif1olem2  22691  efif1olem4  22693  logneg2  22756  cxpsqrtlem  22839  cxpsqrt  22840  logsqrt  22841  1cubr  22929  leibpilem1  23027  leibpilem2  23028  basellem3  23112  ppiub  23235  chtublem  23242  chtub  23243  bcmax  23309  bcp1ctr  23310  bposlem2  23316  bposlem6  23320  bposlem9  23323  logdivsum  23474  4ipval2  25322  4ipval3  25326  ipidsq  25327  dipcl  25329  dipcj  25331  ipasslem11  25459  hvmul0  25645  pjhthlem1  26013  h1de2bi  26176  spanunsni  26201  adjeu  26512  nmopge0  26534  nmfnge0  26550  opsqrlem6  26768  mdsl1i  26944  mdsl2bi  26946  mdexchi  26958  superpos  26977  atabsi  27024  dmdbr5ati  27045  cdj3lem1  27057  fpwrelmapffslem  27255  ogrpaddlt  27398  ofldlt1  27494  ofldchr  27495  oddpwdc  27961  eulerpartgbij  27979  subfacp1lem2a  28292  subfacp1lem5  28296  subfacp1lem6  28297  subfaclim  28300  sinccvglem  28541  binomfallfaclem2  28767  dfon2lem3  28822  dfon2lem7  28826  predeq1  28851  wrecseq1  28944  wsuceq1  28976  bpoly2  29424  bpoly3  29425  fsumcube  29427  sin2h  29650  cos2h  29651  tan2h  29652  opnmbllem0  29655  mblfinlem3  29658  dvtanlem  29669  itg2addnclem3  29673  ftc1cnnclem  29693  ftc1anclem6  29700  ftc2nc  29704  dvasin  29708  clsun  29751  fdc  29869  constcncf  29886  sub1cncf  29888  sub2cncf  29889  heiborlem7  29944  diophren  30379  lhe4.4ex1a  30862  dirkerper  31424  zlmodzxznm  32197  sinh-conventional  32232  dp2cl  32262  dpfrac1  32265  atlatmstc  34134