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  3035  ac6sfi  7117  unfilem1  7137  ordtypelem2  7250  infxpenc2  7665  cda0en  7821  cfsmolem  7912  axdc4lem  8097  1nqenq  8602  mul02lem1  9004  muleqadd  9428  halfcl  9953  rehalfcl  9954  half0  9955  2halves  9956  halfpos2  9957  halfnneg2  9959  halfaddsub  9961  nneo  10111  zeo  10113  peano5uzi  10116  fztp  10857  uzrdgxfr  11045  bcn2  11347  bcpasc  11349  hashxplem  11401  hashfun  11405  swrds2  11576  imre  11609  reim  11610  crim  11616  addcj  11649  imval2  11652  cnpart  11741  sqrlem7  11750  absmax  11829  efgt0  12399  sinf  12420  efi4p  12433  resin4p  12434  recos4p  12435  sinneg  12442  efival  12448  cosadd  12461  sinmul  12468  sinbnd  12476  cosbnd  12477  ef01bndlem  12480  sin01bnd  12481  cos01bnd  12482  sin01gt0  12486  cos01gt0  12487  sin02gt0  12488  rpnnen2lem11  12519  rpnnen2  12520  odd2np1lem  12602  odd2np1  12603  pythagtriplem12  12895  pythagtriplem14  12897  pythagtriplem15  12898  pythagtriplem16  12899  pythagtriplem17  12900  pockthi  12970  prmreclem5  12983  prmreclem6  12984  prmlem0  13123  prdsplusg  13374  prdsmulr  13375  prdsvsca  13376  odinf  14892  lbsexg  15933  mopnex  18081  tngnm  18183  tngngp2  18184  tngngpd  18185  tngngp  18186  iihalf1  18445  iihalf2  18447  pjthlem1  18817  ovolunlem1a  18871  ovolunlem1  18872  opnmbllem  18972  vitalilem4  18982  iblcnlem1  19158  itgcnlem  19160  dvmptre  19334  dvmptim  19335  dvlipcn  19357  aaliou3lem3  19740  aaliou3lem8  19741  sincosq1lem  19881  sincosq2sgn  19883  sincosq3sgn  19884  sincosq4sgn  19885  sinq12gt0  19891  abssinper  19902  coskpi  19904  sineq0  19905  coseq1  19906  efeq1  19907  resinf1o  19914  efif1olem2  19921  efif1olem4  19923  logneg2  19985  cxpsqrlem  20065  cxpsqr  20066  logsqr  20067  1cubr  20154  leibpilem1  20252  leibpilem2  20253  basellem3  20336  ppiub  20459  chtublem  20466  chtub  20467  bcmax  20533  bcp1ctr  20534  bposlem2  20540  bposlem6  20544  bposlem9  20547  logdivsum  20698  4ipval2  21297  4ipval3  21301  ipidsq  21302  dipcl  21304  dipcj  21306  ipasslem11  21434  hvmul0  21619  pjhthlem1  21986  h1de2bi  22149  spanunsni  22174  adjeu  22485  nmopge0  22507  nmfnge0  22523  opsqrlem6  22741  mdsl1i  22917  mdsl2bi  22919  mdexchi  22931  superpos  22950  atabsi  22997  dmdbr5ati  23018  cdj3lem1  23030  subfacp1lem2a  23726  subfacp1lem5  23730  subfacp1lem6  23731  subfaclim  23734  sinccvglem  24020  dfon2lem3  24212  dfon2lem7  24216  bpoly2  24864  bpoly3  24865  fsumcube  24867  itg2addnc  25005  ftc1cnnclem  25024  clsun  26349  fdc  26558  constcncf  26581  addccncf  26582  sub1cncf  26584  sub2cncf  26585  heiborlem7  26644  diophren  26999  psgnghm2  27541  lhe4.4ex1a  27649  sinh-conventional  28463  dp2cl  28493  dpfrac1  28496  atlatmstc  30131
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