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

Theorem mpand 680
Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
Hypotheses
Ref Expression
mpand.1  |-  ( ph  ->  ps )
mpand.2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Assertion
Ref Expression
mpand  |-  ( ph  ->  ( ch  ->  th )
)

Proof of Theorem mpand
StepHypRef Expression
1 mpand.1 . 2  |-  ( ph  ->  ps )
2 mpand.2 . . 3  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
32ancomsd 456 . 2  |-  ( ph  ->  ( ( ch  /\  ps )  ->  th )
)
41, 3mpan2d 679 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
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
This theorem is referenced by:  mpani  681  mp2and  684  ecase2d  949  disjss3  4420  sotri2  5246  ovig  6430  orduniorsuc  6669  omopth2  7291  frfi  7820  ordunifi  7825  finsschain  7885  cantnfp1lem3  8188  cantnfp1  8189  p1le  10450  nnge1  10637  zltp1le  10988  gtndiv  11015  uzss  11181  eluzadd  11189  uzm1  11191  xrre2  11467  xrre3  11468  xrmaxlt  11478  xrmaxle  11480  xrsupsslem  11594  xrub  11599  supxrunb1  11607  elfzoext  11972  flflp1  12044  ceile  12077  seqf1olem1  12253  leexp2r  12331  expnlbnd2  12404  facavg  12487  ccat2s1fvw  12767  caubnd2  13414  limsupbnd1  13537  limsupbnd1OLD  13538  limsupbnd2  13539  limsupbnd2OLD  13540  rlim2lt  13554  rlim3  13555  o1co  13643  mulcn2  13652  cn1lem  13654  rlimo1  13673  climsqz  13697  climsqz2  13698  rlimsqzlem  13705  lo1le  13708  rlimno1  13710  climsup  13726  caucvgrlem2  13733  iseraltlem2  13742  iseralt  13744  fsumabs  13854  cvgcmp  13869  cvgcmpce  13871  isumltss  13899  cvgrat  13932  ruclem9  14283  ruclem12  14286  bitsfzolem  14400  bitsfzolemOLD  14401  bitsfzo  14402  sadcaddlem  14424  gcdeq  14513  algcvgblem  14529  algcvga  14531  lcmdvdsb  14571  lcmftp  14602  coprm  14650  coprmdvds  14652  eulerthlem2  14723  pclem  14781  infpn2  14850  prmreclem1  14853  prmreclem4  14856  ramtlecl  14944  prmgaplem7  15020  initoeu2  15904  lubval  16223  lublecllem  16227  glbval  16236  joinle  16253  latmlem1  16320  odmulg  17200  efginvrel2  17370  pgpfac1lem5  17705  chfacfscmul0  19874  chfacfpmmul0  19878  1stccnp  20469  qustgplem  21127  imasdsf1olem  21380  bldisj  21405  xbln0  21421  prdsbl  21498  metss2lem  21518  stdbdxmet  21522  ngptgp  21636  nghmcn  21758  icoopnst  21959  iocopnst  21960  cnllycmp  21976  iscau3  22240  cmetcaulem  22250  iscmet3lem1  22253  bcthlem4  22287  ovollb2lem  22433  ovolicc2lem3  22464  voliunlem3  22497  volcn  22556  itg10a  22660  itg1ge0a  22661  dvcnvrelem1  22961  dvfsumrlim  22975  itgsubst  22993  ulmcn  23346  ulmdvlem3  23349  mtest  23351  tanord  23479  emcllem6  23918  ftalem2  23990  chtub  24132  fsumvma2  24134  vmasum  24136  chpchtsum  24139  bcmono  24197  bclbnd  24200  bposlem1  24204  bposlem5  24208  bposlem6  24209  lgsne0  24253  chtppilim  24305  dchrisumlem3  24321  pntrsumbnd2  24397  pntlemf  24435  pntlem3  24439  pntleml  24441  redwlklem  25327  eupath2  25700  grpoidinvlem3  25926  grpoideu  25929  vacn  26322  blocni  26438  ubthlem2  26505  chscllem2  27283  lnconi  27678  pjnmopi  27793  atomli  28027  sumdmdlem2  28064  cdj3lem2b  28082  xraddge02  28336  dfon2lem5  30434  dfon2lem6  30435  cgrcoml  30762  btwnconn2  30868  ltflcei  31853  poimirlem2  31862  poimirlem18  31878  poimirlem22  31882  poimirlem23  31883  poimirlem26  31886  poimirlem29  31889  poimirlem30  31890  poimirlem32  31892  heicant  31895  mblfinlem3  31899  mblfinlem4  31900  itg2addnclem  31913  itg2addnc  31916  bddiblnc  31932  ftc1anclem6  31942  ftc1anc  31945  mettrifi  32006  geomcau  32008  equivbnd  32042  heibor1lem  32061  bfplem1  32074  bfplem2  32075  rrncmslem  32084  divrngidl  32181  lecmtN  32747  cvrletrN  32764  llnnleat  33003  lplnnle2at  33031  lvolnle3at  33072  dalem21  33184  cdlemblem  33283  osumcllem11N  33456  pexmidlem8N  33467  lhpmcvr4N  33516  cdleme32b  33934  cdleme35fnpq  33941  cdleme48bw  33994  cdlemf1  34053  cdlemg2fv2  34092  cdlemg7fvbwN  34099  cdlemg27b  34188  tendoeq2  34266  dia2dimlem1  34557  dihord6apre  34749  dihord5apre  34755  dihglbcpreN  34793  dochnel2  34885  dihjat1lem  34921  dochexmidlem8  34960  mapdordlem2  35130  frege124d  36219  climinf  37510  climinfOLD  37511  iccpartlt  38456  gcdzeq  38511  bgoldbtbndlem3  38620  bgoldbtbndlem4  38621  tgoldbach  38629  2ffzoeq  38759  fllog2  39685  dignn0ldlem  39719
  Copyright terms: Public domain W3C validator