Theorem mp3an23 1306

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 1303	. 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  3213  ac6sfi  7548  unfilem1  7568  ordtypelem2  7725  infxpenc2  8180  infxpenc2OLD  8184  cda0en  8340  cfsmolem  8431  axdc4lem  8616  1nqenq  9123  mul02lem1  9537  muleqadd  9972  halfcl  10542  rehalfcl  10543  half0  10544  2halves  10545  halfpos2  10546  halfnneg2  10548  halfaddsub  10550  nneo  10717  zeo  10719  peano5uzi  10722  fztp  11504  uzrdgxfr  11781  bcn2  12087  bcpasc  12089  hashxplem  12187  hashfun  12191  swrds2  12537  repsw2  12542  repsw3  12543  imre  12589  reim  12590  crim  12596  addcj  12629  imval2  12632  cnpart  12721  sqrlem7  12730  absmax  12809  efgt0  13379  sinf  13400  efi4p  13413  resin4p  13414  recos4p  13415  sinneg  13422  efival  13428  cosadd  13441  sinmul  13448  sinbnd  13456  cosbnd  13457  ef01bndlem  13460  sin01bnd  13461  cos01bnd  13462  sin01gt0  13466  cos01gt0  13467  sin02gt0  13468  rpnnen2lem11  13499  rpnnen2  13500  odd2np1lem  13583  odd2np1  13584  pythagtriplem12  13885  pythagtriplem14  13887  pythagtriplem15  13888  pythagtriplem16  13889  pythagtriplem17  13890  pockthi  13960  prmreclem5  13973  prmreclem6  13974  prmlem0  14125  prdsplusg  14388  prdsmulr  14389  prdsvsca  14390  odinf  16055  lbsexg  17222  psgnghm2  17986  mopnex  20069  tngnm  20212  tngngp2  20213  tngngpd  20214  tngngp  20215  addccncf  20467  iihalf1  20478  iihalf2  20480  pjthlem1  20899  ovolunlem1a  20954  ovolunlem1  20955  opnmbllem  21056  vitalilem4  21066  iblcnlem1  21240  itgcnlem  21242  dvmptre  21418  dvmptim  21419  dvlipcn  21441  mdegldg  21512  aaliou3lem3  21785  aaliou3lem8  21786  sincosq1lem  21934  sincosq2sgn  21936  sincosq3sgn  21937  sincosq4sgn  21938  sinq12gt0  21944  abssinper  21955  coskpi  21957  sineq0  21958  coseq1  21959  efeq1  21960  resinf1o  21967  efif1olem2  21974  efif1olem4  21976  logneg2  22039  cxpsqrlem  22122  cxpsqr  22123  logsqr  22124  1cubr  22212  leibpilem1  22310  leibpilem2  22311  basellem3  22395  ppiub  22518  chtublem  22525  chtub  22526  bcmax  22592  bcp1ctr  22593  bposlem2  22599  bposlem6  22603  bposlem9  22606  logdivsum  22757  4ipval2  24054  4ipval3  24058  ipidsq  24059  dipcl  24061  dipcj  24063  ipasslem11  24191  hvmul0  24377  pjhthlem1  24745  h1de2bi  24908  spanunsni  24933  adjeu  25244  nmopge0  25266  nmfnge0  25282  opsqrlem6  25500  mdsl1i  25676  mdsl2bi  25678  mdexchi  25690  superpos  25709  atabsi  25756  dmdbr5ati  25777  cdj3lem1  25789  fpwrelmapffslem  25983  ogrpaddlt  26132  ofldlt1  26232  ofldchr  26233  oddpwdc  26689  eulerpartgbij  26707  subfacp1lem2a  27020  subfacp1lem5  27024  subfacp1lem6  27025  subfaclim  27028  sinccvglem  27268  binomfallfaclem2  27494  dfon2lem3  27549  dfon2lem7  27553  predeq1  27578  wrecseq1  27671  wsuceq1  27703  bpoly2  28151  bpoly3  28152  fsumcube  28154  sin2h  28375  cos2h  28376  tan2h  28377  opnmbllem0  28380  mblfinlem3  28383  dvtanlem  28394  itg2addnclem3  28398  ftc1cnnclem  28418  ftc1anclem6  28425  ftc2nc  28429  dvasin  28433  clsun  28476  fdc  28594  constcncf  28611  sub1cncf  28613  sub2cncf  28614  heiborlem7  28669  diophren  29105  lhe4.4ex1a  29556  zlmodzxznm  30928  sinh-conventional  30963  dp2cl  30993  dpfrac1  30996  atlatmstc  32804