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  4286  sotri2  5222  ovig  6207  orduniorsuc  6436  omopth2  7015  frfi  7549  ordunifi  7554  finsschain  7610  cantnfp1lem3  7880  cantnfp1  7881  cantnfp1lem3OLD  7906  cantnfp1OLD  7907  p1le  10164  nnge1  10340  zltp1le  10686  gtndiv  10711  uzss  10873  eluzadd  10881  uzm1  10883  xrre2  11134  xrre3  11135  xrmaxlt  11145  xrmaxle  11147  xrsupsslem  11261  xrub  11266  supxrunb1  11274  ceile  11680  seqf1olem1  11837  leexp2r  11913  expnlbnd2  11987  facavg  12069  caubnd2  12837  limsupbnd1  12952  limsupbnd2  12953  rlim2lt  12967  rlim3  12968  o1co  13056  mulcn2  13065  cn1lem  13067  rlimo1  13086  climsqz  13110  climsqz2  13111  rlimsqzlem  13118  lo1le  13121  rlimno1  13123  climsup  13139  caucvgrlem2  13144  iseraltlem2  13152  iseralt  13154  fsumabs  13256  cvgcmp  13271  cvgcmpce  13273  isumltss  13303  cvgrat  13335  ruclem9  13512  ruclem12  13515  bitsfzolem  13622  bitsfzo  13623  sadcaddlem  13645  gcdeq  13728  algcvgblem  13744  algcvga  13746  coprm  13778  coprmdvds  13780  eulerthlem2  13849  pclem  13897  infpn2  13966  prmreclem1  13969  prmreclem4  13972  ramtlecl  14053  lubval  15146  lublecllem  15150  glbval  15159  joinle  15176  latmlem1  15243  odmulg  16048  efginvrel2  16215  pgpfac1lem5  16568  1stccnp  19041  divstgplem  19666  imasdsf1olem  19923  bldisj  19948  xbln0  19964  prdsbl  20041  metss2lem  20061  stdbdxmet  20065  ngptgp  20197  nghmcn  20299  icoopnst  20486  iocopnst  20487  cnllycmp  20503  iscau3  20764  cmetcaulem  20774  iscmet3lem1  20777  bcthlem4  20813  ovollb2lem  20946  ovolicc2lem3  20977  voliunlem3  21008  volcn  21061  itg10a  21163  itg1ge0a  21164  dvcnvrelem1  21464  dvfsumrlim  21478  itgsubst  21496  ulmcn  21839  ulmdvlem3  21842  mtest  21844  tanord  21969  emcllem6  22369  ftalem2  22386  chtub  22526  fsumvma2  22528  vmasum  22530  chpchtsum  22533  bcmono  22591  bclbnd  22594  bposlem1  22598  bposlem5  22602  bposlem6  22603  lgsne0  22647  chtppilim  22699  dchrisumlem3  22715  pntrsumbnd2  22791  pntlemf  22829  pntlem3  22833  pntleml  22835  redwlklem  23455  eupath2  23552  grpoidinvlem3  23644  grpoideu  23647  vacn  24040  blocni  24156  ubthlem2  24223  chscllem2  24992  lnconi  25388  pjnmopi  25503  atomli  25737  sumdmdlem2  25774  cdj3lem2b  25792  xraddge02  26001  dfon2lem5  27551  dfon2lem6  27552  cgrcoml  27978  btwnconn2  28084  ltflcei  28372  lxflflp1  28374  heicant  28379  mblfinlem3  28383  mblfinlem4  28384  itg2addnclem  28396  itg2addnc  28399  bddiblnc  28415  ftc1anclem6  28425  ftc1anc  28428  mettrifi  28606  geomcau  28608  equivbnd  28642  heibor1lem  28661  bfplem1  28674  bfplem2  28675  rrncmslem  28684  divrngidl  28781  climinf  29732  2ffzoeq  30167  lecmtN  32741  cvrletrN  32758  llnnleat  32997  lplnnle2at  33025  lvolnle3at  33066  dalem21  33178  cdlemblem  33277  osumcllem11N  33450  pexmidlem8N  33461  lhpmcvr4N  33510  cdleme32b  33926  cdleme35fnpq  33933  cdleme48bw  33986  cdlemf1  34045  cdlemg2fv2  34084  cdlemg7fvbwN  34091  cdlemg27b  34180  tendoeq2  34258  dia2dimlem1  34549  dihord6apre  34741  dihord5apre  34747  dihglbcpreN  34785  dochnel2  34877  dihjat1lem  34913  dochexmidlem8  34952  mapdordlem2  35122
  Copyright terms: Public domain W3C validator