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

Theorem mpand 658
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 442 . 2  |-  ( ph  ->  ( ( ch  /\  ps )  ->  th )
)
41, 3mpan2d 657 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  mpani  659  mp2and  662  ecase2d  908  disjss3  4214  orduniorsuc  4813  sotri2  5266  ovig  6198  omopth2  6830  frfi  7355  ordunifi  7360  finsschain  7416  cantnfp1lem3  7639  cantnfp1  7640  p1le  9858  nnge1  10031  zltp1le  10330  gtndiv  10352  uzss  10511  eluzadd  10519  uzm1  10521  xrre2  10763  xrre3  10764  xrmaxlt  10774  xrmaxle  10776  xrsupsslem  10890  xrub  10895  supxrunb1  10903  ceile  11240  seqf1olem1  11367  leexp2r  11442  expnlbnd2  11515  facavg  11597  caubnd2  12166  limsupbnd1  12281  limsupbnd2  12282  rlim2lt  12296  rlim3  12297  o1co  12385  mulcn2  12394  cn1lem  12396  rlimo1  12415  climsqz  12439  climsqz2  12440  rlimsqzlem  12447  lo1le  12450  rlimno1  12452  climsup  12468  caucvgrlem2  12473  iseraltlem2  12481  iseralt  12483  fsumabs  12585  cvgcmp  12600  cvgcmpce  12602  isumltss  12633  cvgrat  12665  ruclem9  12842  ruclem12  12845  bitsfzolem  12951  bitsfzo  12952  sadcaddlem  12974  gcdeq  13057  algcvgblem  13073  algcvga  13075  coprm  13105  coprmdvds  13107  eulerthlem2  13176  pclem  13217  infpn2  13286  prmreclem1  13289  prmreclem4  13292  ramtlecl  13373  lubid  14444  joinle  14455  latmlem1  14515  odmulg  15197  efginvrel2  15364  pgpfac1lem5  15642  1stccnp  17530  divstgplem  18155  imasdsf1olem  18408  bldisj  18433  xbln0  18449  prdsbl  18526  metss2lem  18546  stdbdxmet  18550  ngptgp  18682  nghmcn  18784  icoopnst  18969  iocopnst  18970  cnllycmp  18986  iscau3  19236  cmetcaulem  19246  iscmet3lem1  19249  bcthlem4  19285  ovollb2lem  19389  ovolicc2lem3  19420  voliunlem3  19451  volcn  19503  itg10a  19605  itg1ge0a  19606  dvcnvrelem1  19906  dvfsumrlim  19920  itgsubst  19938  ulmcn  20320  ulmdvlem3  20323  mtest  20325  tanord  20445  emcllem6  20844  ftalem2  20861  chtub  21001  fsumvma2  21003  vmasum  21005  chpchtsum  21008  bcmono  21066  bclbnd  21069  bposlem1  21073  bposlem5  21077  bposlem6  21078  lgsne0  21122  chtppilim  21174  dchrisumlem3  21190  pntrsumbnd2  21266  pntlemf  21304  pntlem3  21308  pntleml  21310  redwlklem  21610  eupath2  21707  grpoidinvlem3  21799  grpoideu  21802  vacn  22195  blocni  22311  ubthlem2  22378  chscllem2  23145  lnconi  23541  pjnmopi  23656  atomli  23890  sumdmdlem2  23927  cdj3lem2b  23945  xraddge02  24128  dfon2lem5  25419  dfon2lem6  25420  cgrcoml  25935  btwnconn2  26041  ltflcei  26247  lxflflp1  26249  heicant  26253  mblfinlem3  26257  mblfinlem4  26258  itg2addnclem  26270  itg2addnc  26273  bddiblnc  26289  ftc1anclem6  26299  ftc1anc  26302  mettrifi  26477  geomcau  26479  equivbnd  26513  heibor1lem  26532  bfplem1  26545  bfplem2  26546  rrncmslem  26555  divrngidl  26652  climinf  27722  2ffzoeq  28163  lecmtN  30128  cvrletrN  30145  llnnleat  30384  lplnnle2at  30412  lvolnle3at  30453  dalem21  30565  cdlemblem  30664  osumcllem11N  30837  pexmidlem8N  30848  lhpmcvr4N  30897  cdleme32b  31313  cdleme35fnpq  31320  cdleme48bw  31373  cdlemf1  31432  cdlemg2fv2  31471  cdlemg7fvbwN  31478  cdlemg27b  31567  tendoeq2  31645  dia2dimlem1  31936  dihord6apre  32128  dihord5apre  32134  dihglbcpreN  32172  dochnel2  32264  dihjat1lem  32300  dochexmidlem8  32339  mapdordlem2  32509
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 179  df-an 362
  Copyright terms: Public domain W3C validator