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

Theorem mpand 675
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 454 . 2  |-  ( ph  ->  ( ( ch  /\  ps )  ->  th )
)
41, 3mpan2d 674 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  676  mp2and  679  ecase2d  931  disjss3  4398  sotri2  5334  ovig  6321  orduniorsuc  6550  omopth2  7132  frfi  7667  ordunifi  7672  finsschain  7728  cantnfp1lem3  7998  cantnfp1  7999  cantnfp1lem3OLD  8024  cantnfp1OLD  8025  p1le  10282  nnge1  10458  zltp1le  10804  gtndiv  10829  uzss  10991  eluzadd  10999  uzm1  11001  xrre2  11252  xrre3  11253  xrmaxlt  11263  xrmaxle  11265  xrsupsslem  11379  xrub  11384  supxrunb1  11392  ceile  11804  seqf1olem1  11961  leexp2r  12037  expnlbnd2  12111  facavg  12193  caubnd2  12962  limsupbnd1  13077  limsupbnd2  13078  rlim2lt  13092  rlim3  13093  o1co  13181  mulcn2  13190  cn1lem  13192  rlimo1  13211  climsqz  13235  climsqz2  13236  rlimsqzlem  13243  lo1le  13246  rlimno1  13248  climsup  13264  caucvgrlem2  13269  iseraltlem2  13277  iseralt  13279  fsumabs  13381  cvgcmp  13396  cvgcmpce  13398  isumltss  13428  cvgrat  13460  ruclem9  13637  ruclem12  13640  bitsfzolem  13747  bitsfzo  13748  sadcaddlem  13770  gcdeq  13853  algcvgblem  13869  algcvga  13871  coprm  13903  coprmdvds  13905  eulerthlem2  13974  pclem  14022  infpn2  14091  prmreclem1  14094  prmreclem4  14097  ramtlecl  14178  lubval  15272  lublecllem  15276  glbval  15285  joinle  15302  latmlem1  15369  odmulg  16177  efginvrel2  16344  pgpfac1lem5  16701  1stccnp  19197  divstgplem  19822  imasdsf1olem  20079  bldisj  20104  xbln0  20120  prdsbl  20197  metss2lem  20217  stdbdxmet  20221  ngptgp  20353  nghmcn  20455  icoopnst  20642  iocopnst  20643  cnllycmp  20659  iscau3  20920  cmetcaulem  20930  iscmet3lem1  20933  bcthlem4  20969  ovollb2lem  21102  ovolicc2lem3  21133  voliunlem3  21165  volcn  21218  itg10a  21320  itg1ge0a  21321  dvcnvrelem1  21621  dvfsumrlim  21635  itgsubst  21653  ulmcn  21996  ulmdvlem3  21999  mtest  22001  tanord  22126  emcllem6  22526  ftalem2  22543  chtub  22683  fsumvma2  22685  vmasum  22687  chpchtsum  22690  bcmono  22748  bclbnd  22751  bposlem1  22755  bposlem5  22759  bposlem6  22760  lgsne0  22804  chtppilim  22856  dchrisumlem3  22872  pntrsumbnd2  22948  pntlemf  22986  pntlem3  22990  pntleml  22992  redwlklem  23655  eupath2  23752  grpoidinvlem3  23844  grpoideu  23847  vacn  24240  blocni  24356  ubthlem2  24423  chscllem2  25192  lnconi  25588  pjnmopi  25703  atomli  25937  sumdmdlem2  25974  cdj3lem2b  25992  xraddge02  26200  dfon2lem5  27743  dfon2lem6  27744  cgrcoml  28170  btwnconn2  28276  ltflcei  28566  lxflflp1  28568  heicant  28573  mblfinlem3  28577  mblfinlem4  28578  itg2addnclem  28590  itg2addnc  28593  bddiblnc  28609  ftc1anclem6  28619  ftc1anc  28622  mettrifi  28800  geomcau  28802  equivbnd  28836  heibor1lem  28855  bfplem1  28868  bfplem2  28869  rrncmslem  28878  divrngidl  28975  climinf  29926  2ffzoeq  30361  chfacfscmul0  31329  chfacfpmmul0  31333  lecmtN  33224  cvrletrN  33241  llnnleat  33480  lplnnle2at  33508  lvolnle3at  33549  dalem21  33661  cdlemblem  33760  osumcllem11N  33933  pexmidlem8N  33944  lhpmcvr4N  33993  cdleme32b  34409  cdleme35fnpq  34416  cdleme48bw  34469  cdlemf1  34528  cdlemg2fv2  34567  cdlemg7fvbwN  34574  cdlemg27b  34663  tendoeq2  34741  dia2dimlem1  35032  dihord6apre  35224  dihord5apre  35230  dihglbcpreN  35268  dochnel2  35360  dihjat1lem  35396  dochexmidlem8  35435  mapdordlem2  35605
  Copyright terms: Public domain W3C validator