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

Theorem mpand 668
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 451 . 2  |-  ( ph  ->  ( ( ch  /\  ps )  ->  th )
)
41, 3mpan2d 667 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 371
This theorem is referenced by:  mpani  669  mp2and  672  ecase2d  924  disjss3  4279  sotri2  5215  ovig  6201  orduniorsuc  6430  omopth2  7011  frfi  7545  ordunifi  7550  finsschain  7606  cantnfp1lem3  7876  cantnfp1  7877  cantnfp1lem3OLD  7902  cantnfp1OLD  7903  p1le  10160  nnge1  10336  zltp1le  10682  gtndiv  10707  uzss  10869  eluzadd  10877  uzm1  10879  xrre2  11130  xrre3  11131  xrmaxlt  11141  xrmaxle  11143  xrsupsslem  11257  xrub  11262  supxrunb1  11270  ceile  11672  seqf1olem1  11829  leexp2r  11905  expnlbnd2  11979  facavg  12061  caubnd2  12829  limsupbnd1  12944  limsupbnd2  12945  rlim2lt  12959  rlim3  12960  o1co  13048  mulcn2  13057  cn1lem  13059  rlimo1  13078  climsqz  13102  climsqz2  13103  rlimsqzlem  13110  lo1le  13113  rlimno1  13115  climsup  13131  caucvgrlem2  13136  iseraltlem2  13144  iseralt  13146  fsumabs  13247  cvgcmp  13262  cvgcmpce  13264  isumltss  13294  cvgrat  13326  ruclem9  13503  ruclem12  13506  bitsfzolem  13613  bitsfzo  13614  sadcaddlem  13636  gcdeq  13719  algcvgblem  13735  algcvga  13737  coprm  13769  coprmdvds  13771  eulerthlem2  13840  pclem  13888  infpn2  13957  prmreclem1  13960  prmreclem4  13963  ramtlecl  14044  lubval  15137  lublecllem  15141  glbval  15150  joinle  15167  latmlem1  15234  odmulg  16037  efginvrel2  16204  pgpfac1lem5  16554  1stccnp  18908  divstgplem  19533  imasdsf1olem  19790  bldisj  19815  xbln0  19831  prdsbl  19908  metss2lem  19928  stdbdxmet  19932  ngptgp  20064  nghmcn  20166  icoopnst  20353  iocopnst  20354  cnllycmp  20370  iscau3  20631  cmetcaulem  20641  iscmet3lem1  20644  bcthlem4  20680  ovollb2lem  20813  ovolicc2lem3  20844  voliunlem3  20875  volcn  20928  itg10a  21030  itg1ge0a  21031  dvcnvrelem1  21331  dvfsumrlim  21345  itgsubst  21363  ulmcn  21749  ulmdvlem3  21752  mtest  21754  tanord  21879  emcllem6  22279  ftalem2  22296  chtub  22436  fsumvma2  22438  vmasum  22440  chpchtsum  22443  bcmono  22501  bclbnd  22504  bposlem1  22508  bposlem5  22512  bposlem6  22513  lgsne0  22557  chtppilim  22609  dchrisumlem3  22625  pntrsumbnd2  22701  pntlemf  22739  pntlem3  22743  pntleml  22745  redwlklem  23327  eupath2  23424  grpoidinvlem3  23516  grpoideu  23519  vacn  23912  blocni  24028  ubthlem2  24095  chscllem2  24864  lnconi  25260  pjnmopi  25375  atomli  25609  sumdmdlem2  25646  cdj3lem2b  25664  xraddge02  25875  dfon2lem5  27447  dfon2lem6  27448  cgrcoml  27874  btwnconn2  27980  ltflcei  28263  lxflflp1  28265  heicant  28270  mblfinlem3  28274  mblfinlem4  28275  itg2addnclem  28287  itg2addnc  28290  bddiblnc  28306  ftc1anclem6  28316  ftc1anc  28319  mettrifi  28497  geomcau  28499  equivbnd  28533  heibor1lem  28552  bfplem1  28565  bfplem2  28566  rrncmslem  28575  divrngidl  28672  climinf  29625  2ffzoeq  30060  lecmtN  32495  cvrletrN  32512  llnnleat  32751  lplnnle2at  32779  lvolnle3at  32820  dalem21  32932  cdlemblem  33031  osumcllem11N  33204  pexmidlem8N  33215  lhpmcvr4N  33264  cdleme32b  33680  cdleme35fnpq  33687  cdleme48bw  33740  cdlemf1  33799  cdlemg2fv2  33838  cdlemg7fvbwN  33845  cdlemg27b  33934  tendoeq2  34012  dia2dimlem1  34303  dihord6apre  34495  dihord5apre  34501  dihglbcpreN  34539  dochnel2  34631  dihjat1lem  34667  dochexmidlem8  34706  mapdordlem2  34876
  Copyright terms: Public domain W3C validator