MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpand 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
mpand.2
Assertion
Ref Expression
mpand

Proof of Theorem mpand
StepHypRef Expression
1 mpand.1 . 2
2 mpand.2 . . 3
32ancomsd 454 . 2
41, 3mpan2d 674 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  mpani  676  mp2and  679  ecase2d  940  disjss3  4451  sotri2  5401  ovig  6424  orduniorsuc  6665  omopth2  7252  frfi  7785  ordunifi  7790  finsschain  7847  cantnfp1lem3  8120  cantnfp1  8121  cantnfp1lem3OLD  8146  cantnfp1OLD  8147  p1le  10410  nnge1  10587  zltp1le  10938  gtndiv  10965  uzss  11130  eluzadd  11138  uzm1  11140  xrre2  11400  xrre3  11401  xrmaxlt  11411  xrmaxle  11413  xrsupsslem  11527  xrub  11532  supxrunb1  11540  flflp1  11944  ceile  11976  seqf1olem1  12146  leexp2r  12223  expnlbnd2  12297  facavg  12379  caubnd2  13190  limsupbnd1  13305  limsupbnd2  13306  rlim2lt  13320  rlim3  13321  o1co  13409  mulcn2  13418  cn1lem  13420  rlimo1  13439  climsqz  13463  climsqz2  13464  rlimsqzlem  13471  lo1le  13474  rlimno1  13476  climsup  13492  caucvgrlem2  13497  iseraltlem2  13505  iseralt  13507  fsumabs  13615  cvgcmp  13630  cvgcmpce  13632  isumltss  13660  cvgrat  13692  ruclem9  13971  ruclem12  13974  bitsfzolem  14084  bitsfzo  14085  sadcaddlem  14107  gcdeq  14190  algcvgblem  14206  algcvga  14208  coprm  14241  coprmdvds  14243  eulerthlem2  14312  pclem  14362  infpn2  14431  prmreclem1  14434  prmreclem4  14437  ramtlecl  14518  lubval  15614  lublecllem  15618  glbval  15627  joinle  15644  latmlem1  15711  odmulg  16578  efginvrel2  16745  pgpfac1lem5  17130  chfacfscmul0  19359  chfacfpmmul0  19363  1stccnp  19963  qustgplem  20619  imasdsf1olem  20876  bldisj  20901  xbln0  20917  prdsbl  20994  metss2lem  21014  stdbdxmet  21018  ngptgp  21150  nghmcn  21252  icoopnst  21439  iocopnst  21440  cnllycmp  21456  iscau3  21717  cmetcaulem  21727  iscmet3lem1  21730  bcthlem4  21766  ovollb2lem  21899  ovolicc2lem3  21930  voliunlem3  21962  volcn  22015  itg10a  22117  itg1ge0a  22118  dvcnvrelem1  22418  dvfsumrlim  22432  itgsubst  22450  ulmcn  22794  ulmdvlem3  22797  mtest  22799  tanord  22925  emcllem6  23330  ftalem2  23347  chtub  23487  fsumvma2  23489  vmasum  23491  chpchtsum  23494  bcmono  23552  bclbnd  23555  bposlem1  23559  bposlem5  23563  bposlem6  23564  lgsne0  23608  chtppilim  23660  dchrisumlem3  23676  pntrsumbnd2  23752  pntlemf  23790  pntlem3  23794  pntleml  23796  redwlklem  24607  eupath2  24980  grpoidinvlem3  25208  grpoideu  25211  vacn  25604  blocni  25720  ubthlem2  25787  chscllem2  26556  lnconi  26952  pjnmopi  27067  atomli  27301  sumdmdlem2  27338  cdj3lem2b  27356  xraddge02  27577  dfon2lem5  29219  dfon2lem6  29220  cgrcoml  29646  btwnconn2  29752  ltflcei  30043  heicant  30049  mblfinlem3  30053  mblfinlem4  30054  itg2addnclem  30066  itg2addnc  30069  bddiblnc  30085  ftc1anclem6  30095  ftc1anc  30098  mettrifi  30250  geomcau  30252  equivbnd  30286  heibor1lem  30305  bfplem1  30318  bfplem2  30319  rrncmslem  30328  divrngidl  30425  lcmdvdsb  31217  climinf  31612  2ffzoeq  32341  initoeu2  32622  lecmtN  34981  cvrletrN  34998  llnnleat  35237  lplnnle2at  35265  lvolnle3at  35306  dalem21  35418  cdlemblem  35517  osumcllem11N  35690  pexmidlem8N  35701  lhpmcvr4N  35750  cdleme32b  36168  cdleme35fnpq  36175  cdleme48bw  36228  cdlemf1  36287  cdlemg2fv2  36326  cdlemg7fvbwN  36333  cdlemg27b  36422  tendoeq2  36500  dia2dimlem1  36791  dihord6apre  36983  dihord5apre  36989  dihglbcpreN  37027  dochnel2  37119  dihjat1lem  37155  dochexmidlem8  37194  mapdordlem2  37364
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
  Copyright terms: Public domain W3C validator