MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mp3an23 Unicode version

Theorem mp3an23 1269
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
StepHypRef Expression
1 mp3an23.1 . 2  |-  ps
2 mp3an23.2 . . 3  |-  ch
3 mp3an23.3 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
42, 3mp3an3 1266 . 2  |-  ( (
ph  /\  ps )  ->  th )
51, 4mpan2 652 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  sbciegf  3022  ac6sfi  7101  unfilem1  7121  ordtypelem2  7234  infxpenc2  7649  cda0en  7805  cfsmolem  7896  axdc4lem  8081  1nqenq  8586  mul02lem1  8988  muleqadd  9412  halfcl  9937  rehalfcl  9938  half0  9939  2halves  9940  halfpos2  9941  halfnneg2  9943  halfaddsub  9945  nneo  10095  zeo  10097  peano5uzi  10100  fztp  10841  uzrdgxfr  11029  bcn2  11331  bcpasc  11333  hashxplem  11385  hashfun  11389  swrds2  11560  imre  11593  reim  11594  crim  11600  addcj  11633  imval2  11636  cnpart  11725  sqrlem7  11734  absmax  11813  efgt0  12383  sinf  12404  efi4p  12417  resin4p  12418  recos4p  12419  sinneg  12426  efival  12432  cosadd  12445  sinmul  12452  sinbnd  12460  cosbnd  12461  ef01bndlem  12464  sin01bnd  12465  cos01bnd  12466  sin01gt0  12470  cos01gt0  12471  sin02gt0  12472  rpnnen2lem11  12503  rpnnen2  12504  odd2np1lem  12586  odd2np1  12587  pythagtriplem12  12879  pythagtriplem14  12881  pythagtriplem15  12882  pythagtriplem16  12883  pythagtriplem17  12884  pockthi  12954  prmreclem5  12967  prmreclem6  12968  prmlem0  13107  prdsplusg  13358  prdsmulr  13359  prdsvsca  13360  odinf  14876  lbsexg  15917  mopnex  18065  tngnm  18167  tngngp2  18168  tngngpd  18169  tngngp  18170  iihalf1  18429  iihalf2  18431  pjthlem1  18801  ovolunlem1a  18855  ovolunlem1  18856  opnmbllem  18956  vitalilem4  18966  iblcnlem1  19142  itgcnlem  19144  dvmptre  19318  dvmptim  19319  dvlipcn  19341  aaliou3lem3  19724  aaliou3lem8  19725  sincosq1lem  19865  sincosq2sgn  19867  sincosq3sgn  19868  sincosq4sgn  19869  sinq12gt0  19875  abssinper  19886  coskpi  19888  sineq0  19889  coseq1  19890  efeq1  19891  resinf1o  19898  efif1olem2  19905  efif1olem4  19907  logneg2  19969  cxpsqrlem  20049  cxpsqr  20050  logsqr  20051  1cubr  20138  leibpilem1  20236  leibpilem2  20237  basellem3  20320  ppiub  20443  chtublem  20450  chtub  20451  bcmax  20517  bcp1ctr  20518  bposlem2  20524  bposlem6  20528  bposlem9  20531  logdivsum  20682  4ipval2  21281  4ipval3  21285  ipidsq  21286  dipcl  21288  dipcj  21290  ipasslem11  21418  hvmul0  21603  pjhthlem1  21970  h1de2bi  22133  spanunsni  22158  adjeu  22469  nmopge0  22491  nmfnge0  22507  opsqrlem6  22725  mdsl1i  22901  mdsl2bi  22903  mdexchi  22915  superpos  22934  atabsi  22981  dmdbr5ati  23002  cdj3lem1  23014  subfacp1lem2a  23711  subfacp1lem5  23715  subfacp1lem6  23716  subfaclim  23719  sinccvglem  24005  dfon2lem3  24141  dfon2lem7  24145  bpoly2  24792  bpoly3  24793  fsumcube  24795  clsun  26246  fdc  26455  constcncf  26478  addccncf  26479  sub1cncf  26481  sub2cncf  26482  heiborlem7  26541  diophren  26896  psgnghm2  27438  lhe4.4ex1a  27546  sinh-conventional  28209  dp2cl  28239  dpfrac1  28242  atlatmstc  29509
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator