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

Theorem mpand 673
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 452 . 2  |-  ( ph  ->  ( ( ch  /\  ps )  ->  th )
)
41, 3mpan2d 672 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 185  df-an 369
This theorem is referenced by:  mpani  674  mp2and  677  ecase2d  938  disjss3  4438  sotri2  5384  ovig  6397  orduniorsuc  6638  omopth2  7225  frfi  7757  ordunifi  7762  finsschain  7819  cantnfp1lem3  8090  cantnfp1  8091  cantnfp1lem3OLD  8116  cantnfp1OLD  8117  p1le  10381  nnge1  10557  zltp1le  10909  gtndiv  10936  uzss  11102  eluzadd  11110  uzm1  11112  xrre2  11374  xrre3  11375  xrmaxlt  11385  xrmaxle  11387  xrsupsslem  11501  xrub  11506  supxrunb1  11514  elfzoext  11854  flflp1  11925  ceile  11958  seqf1olem1  12128  leexp2r  12205  expnlbnd2  12279  facavg  12361  ccat2s1fvw  12631  caubnd2  13272  limsupbnd1  13387  limsupbnd2  13388  rlim2lt  13402  rlim3  13403  o1co  13491  mulcn2  13500  cn1lem  13502  rlimo1  13521  climsqz  13545  climsqz2  13546  rlimsqzlem  13553  lo1le  13556  rlimno1  13558  climsup  13574  caucvgrlem2  13579  iseraltlem2  13587  iseralt  13589  fsumabs  13697  cvgcmp  13712  cvgcmpce  13714  isumltss  13742  cvgrat  13774  ruclem9  14055  ruclem12  14058  bitsfzolem  14168  bitsfzo  14169  sadcaddlem  14191  gcdeq  14274  algcvgblem  14290  algcvga  14292  coprm  14325  coprmdvds  14327  eulerthlem2  14396  pclem  14446  infpn2  14515  prmreclem1  14518  prmreclem4  14521  ramtlecl  14602  initoeu2  15494  lubval  15813  lublecllem  15817  glbval  15826  joinle  15843  latmlem1  15910  odmulg  16777  efginvrel2  16944  pgpfac1lem5  17325  chfacfscmul0  19526  chfacfpmmul0  19530  1stccnp  20129  qustgplem  20785  imasdsf1olem  21042  bldisj  21067  xbln0  21083  prdsbl  21160  metss2lem  21180  stdbdxmet  21184  ngptgp  21316  nghmcn  21418  icoopnst  21605  iocopnst  21606  cnllycmp  21622  iscau3  21883  cmetcaulem  21893  iscmet3lem1  21896  bcthlem4  21932  ovollb2lem  22065  ovolicc2lem3  22096  voliunlem3  22128  volcn  22181  itg10a  22283  itg1ge0a  22284  dvcnvrelem1  22584  dvfsumrlim  22598  itgsubst  22616  ulmcn  22960  ulmdvlem3  22963  mtest  22965  tanord  23091  emcllem6  23528  ftalem2  23545  chtub  23685  fsumvma2  23687  vmasum  23689  chpchtsum  23692  bcmono  23750  bclbnd  23753  bposlem1  23757  bposlem5  23761  bposlem6  23762  lgsne0  23806  chtppilim  23858  dchrisumlem3  23874  pntrsumbnd2  23950  pntlemf  23988  pntlem3  23992  pntleml  23994  redwlklem  24809  eupath2  25182  grpoidinvlem3  25406  grpoideu  25409  vacn  25802  blocni  25918  ubthlem2  25985  chscllem2  26754  lnconi  27150  pjnmopi  27265  atomli  27499  sumdmdlem2  27536  cdj3lem2b  27554  xraddge02  27808  dfon2lem5  29459  dfon2lem6  29460  cgrcoml  29874  btwnconn2  29980  ltflcei  30283  heicant  30289  mblfinlem3  30293  mblfinlem4  30294  itg2addnclem  30306  itg2addnc  30309  bddiblnc  30325  ftc1anclem6  30335  ftc1anc  30338  mettrifi  30490  geomcau  30492  equivbnd  30526  heibor1lem  30545  bfplem1  30558  bfplem2  30559  rrncmslem  30568  divrngidl  30665  lcmdvdsb  31458  climinf  31851  2ffzoeq  32715  fllog2  33443  dignn0ldlem  33477  lecmtN  35378  cvrletrN  35395  llnnleat  35634  lplnnle2at  35662  lvolnle3at  35703  dalem21  35815  cdlemblem  35914  osumcllem11N  36087  pexmidlem8N  36098  lhpmcvr4N  36147  cdleme32b  36565  cdleme35fnpq  36572  cdleme48bw  36625  cdlemf1  36684  cdlemg2fv2  36723  cdlemg7fvbwN  36730  cdlemg27b  36819  tendoeq2  36897  dia2dimlem1  37188  dihord6apre  37380  dihord5apre  37386  dihglbcpreN  37424  dochnel2  37516  dihjat1lem  37552  dochexmidlem8  37591  mapdordlem2  37761
  Copyright terms: Public domain W3C validator