Theorem mp3an23 1317

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

Syntax hints:   -> wi 4   /\ w3a 974

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 976

This theorem is referenced by:  sbciegf  3345  ac6sfi  7766  unfilem1  7786  ordtypelem2  7947  infxpenc2  8402  infxpenc2OLD  8406  cda0en  8562  cfsmolem  8653  axdc4lem  8838  1nqenq  9343  mul02lem1  9759  muleqadd  10200  halfcl  10771  rehalfcl  10772  half0  10773  2halves  10774  halfpos2  10775  halfnneg2  10777  halfaddsub  10779  nneo  10953  zeo  10955  peano5uzi  10958  fztp  11747  uzrdgxfr  12059  bcn2  12379  bcpasc  12381  hashxplem  12473  hashfun  12477  swrds2  12865  repsw2  12870  repsw3  12871  imre  12923  reim  12924  crim  12930  addcj  12963  imval2  12966  cnpart  13055  sqrlem7  13064  absmax  13144  efgt0  13820  sinf  13841  efi4p  13854  resin4p  13855  recos4p  13856  sinneg  13863  efival  13869  cosadd  13882  sinmul  13889  sinbnd  13897  cosbnd  13898  ef01bndlem  13901  sin01bnd  13902  cos01bnd  13903  sin01gt0  13907  cos01gt0  13908  sin02gt0  13909  rpnnen2lem11  13940  rpnnen2  13941  odd2np1lem  14027  odd2np1  14028  pythagtriplem12  14332  pythagtriplem14  14334  pythagtriplem15  14335  pythagtriplem16  14336  pythagtriplem17  14337  pockthi  14407  prmreclem5  14420  prmreclem6  14421  prmlem0  14573  prdsplusg  14837  prdsmulr  14838  prdsvsca  14839  odinf  16564  lbsexg  17789  psgnghm2  18595  mopnex  21000  tngnm  21143  tngngp2  21144  tngngpd  21145  tngngp  21146  addccncf  21398  iihalf1  21409  iihalf2  21411  pjthlem1  21830  ovolunlem1a  21885  ovolunlem1  21886  opnmbllem  21988  vitalilem4  21998  iblcnlem1  22172  itgcnlem  22174  dvmptre  22350  dvmptim  22351  dvlipcn  22373  mdegldg  22444  aaliou3lem3  22718  aaliou3lem8  22719  sincosq1lem  22868  sincosq2sgn  22870  sincosq3sgn  22871  sincosq4sgn  22872  sinq12gt0  22878  abssinper  22889  coskpi  22891  sineq0  22892  coseq1  22893  efeq1  22894  resinf1o  22901  efif1olem2  22908  efif1olem4  22910  logneg2  22978  cxpsqrtlem  23061  cxpsqrt  23062  logsqrt  23063  1cubr  23151  leibpilem1  23249  leibpilem2  23250  basellem3  23334  ppiub  23457  chtublem  23464  chtub  23465  bcmax  23531  bcp1ctr  23532  bposlem2  23538  bposlem6  23542  bposlem9  23545  logdivsum  23696  4ipval2  25596  4ipval3  25600  ipidsq  25601  dipcl  25603  dipcj  25605  ipasslem11  25733  hvmul0  25919  pjhthlem1  26287  h1de2bi  26450  spanunsni  26475  adjeu  26786  nmopge0  26808  nmfnge0  26824  opsqrlem6  27042  mdsl1i  27218  mdsl2bi  27220  mdexchi  27232  superpos  27251  atabsi  27298  dmdbr5ati  27319  cdj3lem1  27331  fpwrelmapffslem  27533  ogrpaddlt  27686  ofldlt1  27781  ofldchr  27782  oddpwdc  28271  eulerpartgbij  28289  subfacp1lem2a  28602  subfacp1lem5  28606  subfacp1lem6  28607  subfaclim  28610  sinccvglem  29016  binomfallfaclem2  29138  dfon2lem3  29193  dfon2lem7  29197  predeq1  29222  wrecseq1  29315  wsuceq1  29347  bpoly2  29795  bpoly3  29796  fsumcube  29798  sin2h  30021  cos2h  30022  tan2h  30023  opnmbllem0  30026  mblfinlem3  30029  dvtanlem  30040  itg2addnclem3  30044  ftc1cnnclem  30064  ftc1anclem6  30071  ftc2nc  30075  dvasin  30079  clsun  30122  fdc  30214  constcncf  30231  sub1cncf  30233  sub2cncf  30234  heiborlem7  30289  diophren  30723  lhe4.4ex1a  31210  dirkerper  31832  zlmodzxznm  32968  sinh-conventional  33003  dp2cl  33033  dpfrac1  33036  atlatmstc  34919