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  4022  orduniorsuc  4621  sotri2  5072  ovig  5969  omopth2  6582  frfi  7102  ordunifi  7107  finsschain  7162  cantnfp1lem3  7382  cantnfp1  7383  p1le  9599  nnge1  9772  zltp1le  10067  gtndiv  10089  uzss  10248  eluzadd  10256  uzm1  10258  xrre2  10499  xrre3  10500  xrmaxlt  10510  xrmaxle  10512  xrsupsslem  10625  xrub  10630  supxrunb1  10638  ceile  10958  seqf1olem1  11085  leexp2r  11159  expnlbnd2  11232  facavg  11314  caubnd2  11841  limsupbnd1  11956  limsupbnd2  11957  rlim2lt  11971  rlim3  11972  o1co  12060  mulcn2  12069  cn1lem  12071  rlimo1  12090  climsqz  12114  climsqz2  12115  rlimsqzlem  12122  lo1le  12125  rlimno1  12127  climsup  12143  caucvgrlem2  12147  iseraltlem2  12155  iseralt  12157  fsumabs  12259  cvgcmp  12274  cvgcmpce  12276  isumltss  12307  cvgrat  12339  ruclem9  12516  ruclem12  12519  bitsfzolem  12625  bitsfzo  12626  sadcaddlem  12648  gcdeq  12731  algcvgblem  12747  algcvga  12749  coprm  12779  coprmdvds  12781  eulerthlem2  12850  pclem  12891  infpn2  12960  prmreclem1  12963  prmreclem4  12966  ramtlecl  13047  lubid  14116  joinle  14127  latmlem1  14187  odmulg  14869  efginvrel2  15036  pgpfac1lem5  15314  1stccnp  17188  divstgplem  17803  imasdsf1olem  17937  bldisj  17955  xbln0  17965  prdsbl  18037  metss2lem  18057  stdbdxmet  18061  ngptgp  18152  nghmcn  18254  icoopnst  18437  iocopnst  18438  cnllycmp  18454  iscau3  18704  cmetcaulem  18714  iscmet3lem1  18717  bcthlem4  18749  ovollb2lem  18847  ovolicc2lem3  18878  voliunlem3  18909  volcn  18961  itg10a  19065  itg1ge0a  19066  dvcnvrelem1  19364  dvfsumrlim  19378  itgsubst  19396  ulmcn  19776  ulmdvlem3  19779  mtest  19781  tanord  19900  emcllem6  20294  ftalem2  20311  chtub  20451  fsumvma2  20453  vmasum  20455  chpchtsum  20458  bcmono  20516  bclbnd  20519  bposlem1  20523  bposlem5  20527  bposlem6  20528  lgsne0  20572  chtppilim  20624  dchrisumlem3  20640  pntrsumbnd2  20716  pntlemf  20754  pntlem3  20758  pntleml  20760  grpoidinvlem3  20873  grpoideu  20876  vacn  21267  blocni  21383  ubthlem2  21450  chscllem2  22217  lnconi  22613  pjnmopi  22728  atomli  22962  sumdmdlem2  22999  cdj3lem2b  23017  xrre3FL  23251  xraddge02  23252  eupath2  23904  dfon2lem5  24143  dfon2lem6  24144  cgrcoml  24619  btwnconn2  24725  clscnc  26010  mettrifi  26473  geomcau  26475  equivbnd  26514  heibor1lem  26533  bfplem1  26546  bfplem2  26547  rrncmslem  26556  divrngidl  26653  climinf  27732  lecmtN  29446  cvrletrN  29463  llnnleat  29702  lplnnle2at  29730  lvolnle3at  29771  dalem21  29883  cdlemblem  29982  osumcllem11N  30155  pexmidlem8N  30166  lhpmcvr4N  30215  cdleme32b  30631  cdleme35fnpq  30638  cdleme48bw  30691  cdlemf1  30750  cdlemg2fv2  30789  cdlemg7fvbwN  30796  cdlemg27b  30885  tendoeq2  30963  dia2dimlem1  31254  dihord6apre  31446  dihord5apre  31452  dihglbcpreN  31490  dochnel2  31582  dihjat1lem  31618  dochexmidlem8  31657  mapdordlem2  31827
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