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

Theorem mpand 657
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 441 . 2  |-  ( ph  ->  ( ( ch  /\  ps )  ->  th )
)
41, 3mpan2d 656 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  mpani  658  mp2and  661  ecase2d  907  disjss3  4152  orduniorsuc  4750  sotri2  5203  ovig  6134  omopth2  6763  frfi  7288  ordunifi  7293  finsschain  7348  cantnfp1lem3  7569  cantnfp1  7570  p1le  9785  nnge1  9958  zltp1le  10257  gtndiv  10279  uzss  10438  eluzadd  10446  uzm1  10448  xrre2  10690  xrre3  10691  xrmaxlt  10701  xrmaxle  10703  xrsupsslem  10817  xrub  10822  supxrunb1  10830  ceile  11162  seqf1olem1  11289  leexp2r  11364  expnlbnd2  11437  facavg  11519  caubnd2  12088  limsupbnd1  12203  limsupbnd2  12204  rlim2lt  12218  rlim3  12219  o1co  12307  mulcn2  12316  cn1lem  12318  rlimo1  12337  climsqz  12361  climsqz2  12362  rlimsqzlem  12369  lo1le  12372  rlimno1  12374  climsup  12390  caucvgrlem2  12395  iseraltlem2  12403  iseralt  12405  fsumabs  12507  cvgcmp  12522  cvgcmpce  12524  isumltss  12555  cvgrat  12587  ruclem9  12764  ruclem12  12767  bitsfzolem  12873  bitsfzo  12874  sadcaddlem  12896  gcdeq  12979  algcvgblem  12995  algcvga  12997  coprm  13027  coprmdvds  13029  eulerthlem2  13098  pclem  13139  infpn2  13208  prmreclem1  13211  prmreclem4  13214  ramtlecl  13295  lubid  14366  joinle  14377  latmlem1  14437  odmulg  15119  efginvrel2  15286  pgpfac1lem5  15564  1stccnp  17446  divstgplem  18071  imasdsf1olem  18311  bldisj  18329  xbln0  18339  prdsbl  18411  metss2lem  18431  stdbdxmet  18435  ngptgp  18548  nghmcn  18650  icoopnst  18835  iocopnst  18836  cnllycmp  18852  iscau3  19102  cmetcaulem  19112  iscmet3lem1  19115  bcthlem4  19149  ovollb2lem  19251  ovolicc2lem3  19282  voliunlem3  19313  volcn  19365  itg10a  19469  itg1ge0a  19470  dvcnvrelem1  19768  dvfsumrlim  19782  itgsubst  19800  ulmcn  20182  ulmdvlem3  20185  mtest  20187  tanord  20307  emcllem6  20706  ftalem2  20723  chtub  20863  fsumvma2  20865  vmasum  20867  chpchtsum  20870  bcmono  20928  bclbnd  20931  bposlem1  20935  bposlem5  20939  bposlem6  20940  lgsne0  20984  chtppilim  21036  dchrisumlem3  21052  pntrsumbnd2  21128  pntlemf  21166  pntlem3  21170  pntleml  21172  redwlklem  21453  eupath2  21550  grpoidinvlem3  21642  grpoideu  21645  vacn  22038  blocni  22154  ubthlem2  22221  chscllem2  22988  lnconi  23384  pjnmopi  23499  atomli  23733  sumdmdlem2  23770  cdj3lem2b  23788  xraddge02  23959  dfon2lem5  25167  dfon2lem6  25168  cgrcoml  25644  btwnconn2  25750  ltflcei  25950  lxflflp1  25952  itg2addnclem  25957  itg2addnc  25959  bddiblnc  25975  mettrifi  26154  geomcau  26156  equivbnd  26190  heibor1lem  26209  bfplem1  26222  bfplem2  26223  rrncmslem  26232  divrngidl  26329  climinf  27400  lecmtN  29371  cvrletrN  29388  llnnleat  29627  lplnnle2at  29655  lvolnle3at  29696  dalem21  29808  cdlemblem  29907  osumcllem11N  30080  pexmidlem8N  30091  lhpmcvr4N  30140  cdleme32b  30556  cdleme35fnpq  30563  cdleme48bw  30616  cdlemf1  30675  cdlemg2fv2  30714  cdlemg7fvbwN  30721  cdlemg27b  30810  tendoeq2  30888  dia2dimlem1  31179  dihord6apre  31371  dihord5apre  31377  dihglbcpreN  31415  dochnel2  31507  dihjat1lem  31543  dochexmidlem8  31582  mapdordlem2  31752
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
  Copyright terms: Public domain W3C validator