Theorem mp3an23 1307

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

Syntax hints:   -> wi 4   /\ w3a 965

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 967

This theorem is referenced by:  sbciegf  3324  ac6sfi  7666  unfilem1  7686  ordtypelem2  7843  infxpenc2  8298  infxpenc2OLD  8302  cda0en  8458  cfsmolem  8549  axdc4lem  8734  1nqenq  9241  mul02lem1  9655  muleqadd  10090  halfcl  10660  rehalfcl  10661  half0  10662  2halves  10663  halfpos2  10664  halfnneg2  10666  halfaddsub  10668  nneo  10835  zeo  10837  peano5uzi  10840  fztp  11628  uzrdgxfr  11905  bcn2  12211  bcpasc  12213  hashxplem  12312  hashfun  12316  swrds2  12662  repsw2  12667  repsw3  12668  imre  12714  reim  12715  crim  12721  addcj  12754  imval2  12757  cnpart  12846  sqrlem7  12855  absmax  12934  efgt0  13504  sinf  13525  efi4p  13538  resin4p  13539  recos4p  13540  sinneg  13547  efival  13553  cosadd  13566  sinmul  13573  sinbnd  13581  cosbnd  13582  ef01bndlem  13585  sin01bnd  13586  cos01bnd  13587  sin01gt0  13591  cos01gt0  13592  sin02gt0  13593  rpnnen2lem11  13624  rpnnen2  13625  odd2np1lem  13708  odd2np1  13709  pythagtriplem12  14010  pythagtriplem14  14012  pythagtriplem15  14013  pythagtriplem16  14014  pythagtriplem17  14015  pockthi  14085  prmreclem5  14098  prmreclem6  14099  prmlem0  14250  prdsplusg  14514  prdsmulr  14515  prdsvsca  14516  odinf  16184  lbsexg  17367  psgnghm2  18135  mopnex  20225  tngnm  20368  tngngp2  20369  tngngpd  20370  tngngp  20371  addccncf  20623  iihalf1  20634  iihalf2  20636  pjthlem1  21055  ovolunlem1a  21110  ovolunlem1  21111  opnmbllem  21213  vitalilem4  21223  iblcnlem1  21397  itgcnlem  21399  dvmptre  21575  dvmptim  21576  dvlipcn  21598  mdegldg  21669  aaliou3lem3  21942  aaliou3lem8  21943  sincosq1lem  22091  sincosq2sgn  22093  sincosq3sgn  22094  sincosq4sgn  22095  sinq12gt0  22101  abssinper  22112  coskpi  22114  sineq0  22115  coseq1  22116  efeq1  22117  resinf1o  22124  efif1olem2  22131  efif1olem4  22133  logneg2  22196  cxpsqrlem  22279  cxpsqr  22280  logsqr  22281  1cubr  22369  leibpilem1  22467  leibpilem2  22468  basellem3  22552  ppiub  22675  chtublem  22682  chtub  22683  bcmax  22749  bcp1ctr  22750  bposlem2  22756  bposlem6  22760  bposlem9  22763  logdivsum  22914  4ipval2  24254  4ipval3  24258  ipidsq  24259  dipcl  24261  dipcj  24263  ipasslem11  24391  hvmul0  24577  pjhthlem1  24945  h1de2bi  25108  spanunsni  25133  adjeu  25444  nmopge0  25466  nmfnge0  25482  opsqrlem6  25700  mdsl1i  25876  mdsl2bi  25878  mdexchi  25890  superpos  25909  atabsi  25956  dmdbr5ati  25977  cdj3lem1  25989  fpwrelmapffslem  26182  ogrpaddlt  26325  ofldlt1  26425  ofldchr  26426  oddpwdc  26880  eulerpartgbij  26898  subfacp1lem2a  27211  subfacp1lem5  27215  subfacp1lem6  27216  subfaclim  27219  sinccvglem  27460  binomfallfaclem2  27686  dfon2lem3  27741  dfon2lem7  27745  predeq1  27770  wrecseq1  27863  wsuceq1  27895  bpoly2  28343  bpoly3  28344  fsumcube  28346  sin2h  28569  cos2h  28570  tan2h  28571  opnmbllem0  28574  mblfinlem3  28577  dvtanlem  28588  itg2addnclem3  28592  ftc1cnnclem  28612  ftc1anclem6  28619  ftc2nc  28623  dvasin  28627  clsun  28670  fdc  28788  constcncf  28805  sub1cncf  28807  sub2cncf  28808  heiborlem7  28863  diophren  29299  lhe4.4ex1a  29750  zlmodzxznm  31157  sinh-conventional  31387  dp2cl  31417  dpfrac1  31420  atlatmstc  33287