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

Theorem mpand 656
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 440 . 2  |-  ( ph  ->  ( ( ch  /\  ps )  ->  th )
)
41, 3mpan2d 655 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  mpani  657  mp2and  660  ecase2d  906  disjss3  4038  orduniorsuc  4637  sotri2  5088  ovig  5985  omopth2  6598  frfi  7118  ordunifi  7123  finsschain  7178  cantnfp1lem3  7398  cantnfp1  7399  p1le  9615  nnge1  9788  zltp1le  10083  gtndiv  10105  uzss  10264  eluzadd  10272  uzm1  10274  xrre2  10515  xrre3  10516  xrmaxlt  10526  xrmaxle  10528  xrsupsslem  10641  xrub  10646  supxrunb1  10654  ceile  10974  seqf1olem1  11101  leexp2r  11175  expnlbnd2  11248  facavg  11330  caubnd2  11857  limsupbnd1  11972  limsupbnd2  11973  rlim2lt  11987  rlim3  11988  o1co  12076  mulcn2  12085  cn1lem  12087  rlimo1  12106  climsqz  12130  climsqz2  12131  rlimsqzlem  12138  lo1le  12141  rlimno1  12143  climsup  12159  caucvgrlem2  12163  iseraltlem2  12171  iseralt  12173  fsumabs  12275  cvgcmp  12290  cvgcmpce  12292  isumltss  12323  cvgrat  12355  ruclem9  12532  ruclem12  12535  bitsfzolem  12641  bitsfzo  12642  sadcaddlem  12664  gcdeq  12747  algcvgblem  12763  algcvga  12765  coprm  12795  coprmdvds  12797  eulerthlem2  12866  pclem  12907  infpn2  12976  prmreclem1  12979  prmreclem4  12982  ramtlecl  13063  lubid  14132  joinle  14143  latmlem1  14203  odmulg  14885  efginvrel2  15052  pgpfac1lem5  15330  1stccnp  17204  divstgplem  17819  imasdsf1olem  17953  bldisj  17971  xbln0  17981  prdsbl  18053  metss2lem  18073  stdbdxmet  18077  ngptgp  18168  nghmcn  18270  icoopnst  18453  iocopnst  18454  cnllycmp  18470  iscau3  18720  cmetcaulem  18730  iscmet3lem1  18733  bcthlem4  18765  ovollb2lem  18863  ovolicc2lem3  18894  voliunlem3  18925  volcn  18977  itg10a  19081  itg1ge0a  19082  dvcnvrelem1  19380  dvfsumrlim  19394  itgsubst  19412  ulmcn  19792  ulmdvlem3  19795  mtest  19797  tanord  19916  emcllem6  20310  ftalem2  20327  chtub  20467  fsumvma2  20469  vmasum  20471  chpchtsum  20474  bcmono  20532  bclbnd  20535  bposlem1  20539  bposlem5  20543  bposlem6  20544  lgsne0  20588  chtppilim  20640  dchrisumlem3  20656  pntrsumbnd2  20732  pntlemf  20770  pntlem3  20774  pntleml  20776  grpoidinvlem3  20889  grpoideu  20892  vacn  21283  blocni  21399  ubthlem2  21466  chscllem2  22233  lnconi  22629  pjnmopi  22744  atomli  22978  sumdmdlem2  23015  cdj3lem2b  23033  xrre3FL  23266  xraddge02  23267  eupath2  23919  dfon2lem5  24214  dfon2lem6  24215  cgrcoml  24691  btwnconn2  24797  ltflcei  24998  lxflflp1  25000  itg2addnclem  25003  itg2addnc  25005  bddiblnc  25021  clscnc  26113  mettrifi  26576  geomcau  26578  equivbnd  26617  heibor1lem  26636  bfplem1  26649  bfplem2  26650  rrncmslem  26659  divrngidl  26756  climinf  27835  redwlklem  28363  lecmtN  30068  cvrletrN  30085  llnnleat  30324  lplnnle2at  30352  lvolnle3at  30393  dalem21  30505  cdlemblem  30604  osumcllem11N  30777  pexmidlem8N  30788  lhpmcvr4N  30837  cdleme32b  31253  cdleme35fnpq  31260  cdleme48bw  31313  cdlemf1  31372  cdlemg2fv2  31411  cdlemg7fvbwN  31418  cdlemg27b  31507  tendoeq2  31585  dia2dimlem1  31876  dihord6apre  32068  dihord5apre  32074  dihglbcpreN  32112  dochnel2  32204  dihjat1lem  32240  dochexmidlem8  32279  mapdordlem2  32449
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 177  df-an 360
  Copyright terms: Public domain W3C validator