Theorem mp3an23 1353

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

Syntax hints:   -> wi 4   /\ w3a 983

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 189  df-an 373  df-3an 985

This theorem is referenced by:  sbciegf  3332  predeq1  5399  wrecseq1  7037  ac6sfi  7819  unfilem1  7839  ordtypelem2  8038  infxpenc2  8455  cda0en  8611  cfsmolem  8702  axdc4lem  8887  1nqenq  9389  mul02lem1  9811  muleqadd  10258  halfcl  10840  rehalfcl  10841  half0  10842  2halves  10843  halfpos2  10844  halfnneg2  10846  halfaddsub  10848  nneo  11021  zeo  11023  peano5uzi  11026  fztp  11854  uzrdgxfr  12181  bcn2  12505  bcpasc  12507  hashxplem  12604  hashfun  12608  swrds2  13014  repsw2  13019  repsw3  13020  imre  13165  reim  13166  crim  13172  addcj  13205  imval2  13208  cnpart  13297  sqrlem7  13306  absmax  13386  binomfallfaclem2  14086  bpoly2  14103  bpoly3  14104  fsumcube  14106  efgt0  14150  sinf  14171  efi4p  14184  resin4p  14185  recos4p  14186  sinneg  14193  efival  14199  cosadd  14212  sinmul  14219  sinbnd  14227  cosbnd  14228  ef01bndlem  14231  sin01bnd  14232  cos01bnd  14233  sin01gt0  14237  cos01gt0  14238  sin02gt0  14239  rpnnen2lem11  14270  rpnnen2  14271  odd2np1lem  14357  odd2np1  14358  pythagtriplem12  14769  pythagtriplem14  14771  pythagtriplem15  14772  pythagtriplem16  14773  pythagtriplem17  14774  pockthi  14844  prmreclem5  14857  prmreclem6  14858  prmlem0  15070  prdsplusg  15349  prdsmulr  15350  prdsvsca  15351  odinf  17207  lbsexg  18380  psgnghm2  19141  mopnex  21526  tngnm  21651  tngngp2  21652  tngngpd  21653  tngngp  21654  addccncf  21940  iihalf1  21951  iihalf2  21953  pjthlem1  22383  ovolunlem1a  22441  ovolunlem1  22442  opnmbllem  22551  vitalilem4  22561  iblcnlem1  22737  itgcnlem  22739  dvmptre  22915  dvmptim  22916  dvlipcn  22938  mdegldg  23007  aaliou3lem3  23292  aaliou3lem8  23293  sincosq1lem  23444  sincosq2sgn  23446  sincosq3sgn  23447  sincosq4sgn  23448  sinq12gt0  23454  abssinper  23465  coskpi  23467  sineq0  23468  coseq1  23469  efeq1  23470  resinf1o  23477  efif1olem2  23484  efif1olem4  23486  logneg2  23556  cxpsqrtlem  23639  cxpsqrt  23640  logsqrt  23641  1cubr  23760  leibpilem1  23858  leibpilem2  23859  basellem3  24001  ppiub  24124  chtublem  24131  chtub  24132  bcmax  24198  bcp1ctr  24199  bposlem2  24205  bposlem6  24209  bposlem9  24212  logdivsum  24363  4ipval2  26336  4ipval3  26340  ipidsq  26341  dipcl  26343  dipcj  26345  ipasslem11  26473  hvmul0  26669  pjhthlem1  27036  h1de2bi  27199  spanunsni  27224  adjeu  27534  nmopge0  27556  nmfnge0  27572  opsqrlem6  27790  mdsl1i  27966  mdsl2bi  27968  mdexchi  27980  superpos  27999  atabsi  28046  dmdbr5ati  28067  cdj3lem1  28079  fpwrelmapffslem  28317  ogrpaddlt  28482  ofldlt1  28578  ofldchr  28579  oddpwdc  29189  eulerpartgbij  29207  subfacp1lem2a  29905  subfacp1lem5  29909  subfacp1lem6  29910  subfaclim  29913  sinccvglem  30318  dfon2lem3  30432  dfon2lem7  30436  wsuceq1  30499  clsun  30983  vtoclefex  31694  finxpreclem5  31745  sin2h  31893  cos2h  31894  tan2h  31895  poimirlem22  31920  poimirlem26  31924  poimirlem31  31929  opnmbllem0  31934  mblfinlem3  31937  dvtanlemOLD  31949  itg2addnclem3  31953  ftc1cnnclem  31973  ftc1anclem6  31980  ftc2nc  31984  dvasin  31986  fdc  32032  constcncf  32049  sub1cncf  32051  sub2cncf  32052  heiborlem7  32107  atlatmstc  32848  diophren  35619  dftrcl3  36216  dfrtrcl3  36229  cotrclrcl  36238  lhe4.4ex1a  36580  dirkerper  37822  zlmodzxznm  39634  sinh-conventional  39803  dp2cl  39833  dpfrac1  39836