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

Theorem mp3an23 1271
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 1268 . 2  |-  ( (
ph  /\  ps )  ->  th )
51, 4mpan2 653 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  sbciegf  3184  ac6sfi  7343  unfilem1  7363  ordtypelem2  7480  infxpenc2  7895  cda0en  8051  cfsmolem  8142  axdc4lem  8327  1nqenq  8831  mul02lem1  9234  muleqadd  9658  halfcl  10185  rehalfcl  10186  half0  10187  2halves  10188  halfpos2  10189  halfnneg2  10191  halfaddsub  10193  nneo  10345  zeo  10347  peano5uzi  10350  fztp  11094  uzrdgxfr  11298  bcn2  11602  bcpasc  11604  hashxplem  11688  hashfun  11692  swrds2  11872  imre  11905  reim  11906  crim  11912  addcj  11945  imval2  11948  cnpart  12037  sqrlem7  12046  absmax  12125  efgt0  12696  sinf  12717  efi4p  12730  resin4p  12731  recos4p  12732  sinneg  12739  efival  12745  cosadd  12758  sinmul  12765  sinbnd  12773  cosbnd  12774  ef01bndlem  12777  sin01bnd  12778  cos01bnd  12779  sin01gt0  12783  cos01gt0  12784  sin02gt0  12785  rpnnen2lem11  12816  rpnnen2  12817  odd2np1lem  12899  odd2np1  12900  pythagtriplem12  13192  pythagtriplem14  13194  pythagtriplem15  13195  pythagtriplem16  13196  pythagtriplem17  13197  pockthi  13267  prmreclem5  13280  prmreclem6  13281  prmlem0  13420  prdsplusg  13673  prdsmulr  13674  prdsvsca  13675  odinf  15191  lbsexg  16228  mopnex  18541  tngnm  18684  tngngp2  18685  tngngpd  18686  tngngp  18687  addccncf  18938  iihalf1  18948  iihalf2  18950  pjthlem1  19330  ovolunlem1a  19384  ovolunlem1  19385  opnmbllem  19485  vitalilem4  19495  iblcnlem1  19671  itgcnlem  19673  dvmptre  19847  dvmptim  19848  dvlipcn  19870  aaliou3lem3  20253  aaliou3lem8  20254  sincosq1lem  20397  sincosq2sgn  20399  sincosq3sgn  20400  sincosq4sgn  20401  sinq12gt0  20407  abssinper  20418  coskpi  20420  sineq0  20421  coseq1  20422  efeq1  20423  resinf1o  20430  efif1olem2  20437  efif1olem4  20439  logneg2  20502  cxpsqrlem  20585  cxpsqr  20586  logsqr  20587  1cubr  20674  leibpilem1  20772  leibpilem2  20773  basellem3  20857  ppiub  20980  chtublem  20987  chtub  20988  bcmax  21054  bcp1ctr  21055  bposlem2  21061  bposlem6  21065  bposlem9  21068  logdivsum  21219  4ipval2  22196  4ipval3  22200  ipidsq  22201  dipcl  22203  dipcj  22205  ipasslem11  22333  hvmul0  22518  pjhthlem1  22885  h1de2bi  23048  spanunsni  23073  adjeu  23384  nmopge0  23406  nmfnge0  23422  opsqrlem6  23640  mdsl1i  23816  mdsl2bi  23818  mdexchi  23830  superpos  23849  atabsi  23896  dmdbr5ati  23917  cdj3lem1  23929  ofldaddlt  24233  ofldlt1  24235  ofldchr  24236  subfacp1lem2a  24858  subfacp1lem5  24862  subfacp1lem6  24863  subfaclim  24866  sinccvglem  25101  binomfallfaclem2  25348  dfon2lem3  25404  dfon2lem7  25408  predeq1  25433  wrecseq1  25526  wsuceq1  25558  bpoly2  26095  bpoly3  26096  fsumcube  26098  mblfinlem  26234  mblfinlem2  26235  itg2addnclem3  26248  ftc1cnnclem  26268  ftc1anclem6  26275  ftc2nc  26279  clsun  26322  fdc  26440  constcncf  26459  sub1cncf  26461  sub2cncf  26462  heiborlem7  26517  diophren  26865  psgnghm2  27406  lhe4.4ex1a  27514  sinh-conventional  28419  dp2cl  28449  dpfrac1  28452  atlatmstc  30054
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator