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

Theorem mpand 657
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 441 . 2  |-  ( ph  ->  ( ( ch  /\  ps )  ->  th )
)
41, 3mpan2d 656 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  mpani  658  mp2and  661  ecase2d  907  disjss3  4203  orduniorsuc  4802  sotri2  5255  ovig  6187  omopth2  6819  frfi  7344  ordunifi  7349  finsschain  7405  cantnfp1lem3  7628  cantnfp1  7629  p1le  9845  nnge1  10018  zltp1le  10317  gtndiv  10339  uzss  10498  eluzadd  10506  uzm1  10508  xrre2  10750  xrre3  10751  xrmaxlt  10761  xrmaxle  10763  xrsupsslem  10877  xrub  10882  supxrunb1  10890  ceile  11227  seqf1olem1  11354  leexp2r  11429  expnlbnd2  11502  facavg  11584  caubnd2  12153  limsupbnd1  12268  limsupbnd2  12269  rlim2lt  12283  rlim3  12284  o1co  12372  mulcn2  12381  cn1lem  12383  rlimo1  12402  climsqz  12426  climsqz2  12427  rlimsqzlem  12434  lo1le  12437  rlimno1  12439  climsup  12455  caucvgrlem2  12460  iseraltlem2  12468  iseralt  12470  fsumabs  12572  cvgcmp  12587  cvgcmpce  12589  isumltss  12620  cvgrat  12652  ruclem9  12829  ruclem12  12832  bitsfzolem  12938  bitsfzo  12939  sadcaddlem  12961  gcdeq  13044  algcvgblem  13060  algcvga  13062  coprm  13092  coprmdvds  13094  eulerthlem2  13163  pclem  13204  infpn2  13273  prmreclem1  13276  prmreclem4  13279  ramtlecl  13360  lubid  14431  joinle  14442  latmlem1  14502  odmulg  15184  efginvrel2  15351  pgpfac1lem5  15629  1stccnp  17517  divstgplem  18142  imasdsf1olem  18395  bldisj  18420  xbln0  18436  prdsbl  18513  metss2lem  18533  stdbdxmet  18537  ngptgp  18669  nghmcn  18771  icoopnst  18956  iocopnst  18957  cnllycmp  18973  iscau3  19223  cmetcaulem  19233  iscmet3lem1  19236  bcthlem4  19272  ovollb2lem  19376  ovolicc2lem3  19407  voliunlem3  19438  volcn  19490  itg10a  19594  itg1ge0a  19595  dvcnvrelem1  19893  dvfsumrlim  19907  itgsubst  19925  ulmcn  20307  ulmdvlem3  20310  mtest  20312  tanord  20432  emcllem6  20831  ftalem2  20848  chtub  20988  fsumvma2  20990  vmasum  20992  chpchtsum  20995  bcmono  21053  bclbnd  21056  bposlem1  21060  bposlem5  21064  bposlem6  21065  lgsne0  21109  chtppilim  21161  dchrisumlem3  21177  pntrsumbnd2  21253  pntlemf  21291  pntlem3  21295  pntleml  21297  redwlklem  21597  eupath2  21694  grpoidinvlem3  21786  grpoideu  21789  vacn  22182  blocni  22298  ubthlem2  22365  chscllem2  23132  lnconi  23528  pjnmopi  23643  atomli  23877  sumdmdlem2  23914  cdj3lem2b  23932  xraddge02  24115  dfon2lem5  25406  dfon2lem6  25407  cgrcoml  25922  btwnconn2  26028  ltflcei  26231  lxflflp1  26233  mblfinlem2  26235  mblfinlem3  26236  itg2addnclem  26246  itg2addnc  26249  bddiblnc  26265  ftc1anclem6  26275  ftc1anc  26278  mettrifi  26454  geomcau  26456  equivbnd  26490  heibor1lem  26509  bfplem1  26522  bfplem2  26523  rrncmslem  26532  divrngidl  26629  climinf  27699  lecmtN  29991  cvrletrN  30008  llnnleat  30247  lplnnle2at  30275  lvolnle3at  30316  dalem21  30428  cdlemblem  30527  osumcllem11N  30700  pexmidlem8N  30711  lhpmcvr4N  30760  cdleme32b  31176  cdleme35fnpq  31183  cdleme48bw  31236  cdlemf1  31295  cdlemg2fv2  31334  cdlemg7fvbwN  31341  cdlemg27b  31430  tendoeq2  31508  dia2dimlem1  31799  dihord6apre  31991  dihord5apre  31997  dihglbcpreN  32035  dochnel2  32127  dihjat1lem  32163  dochexmidlem8  32202  mapdordlem2  32372
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator