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

Theorem mpand 694
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 469 . 2 (𝜑 → ((𝜒𝜓) → 𝜃))
41, 3mpan2d 693 1 (𝜑 → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  mpani  695  mp2and  698  ecase2d  1027  disjss3  5029  sotri2  5956  fpropnf1  7003  ovig  7275  orduniorsuc  7525  omopth2  8193  frfi  8747  ordunifi  8752  finsschain  8815  cantnfp1lem3  9127  cantnfp1  9128  p1le  11474  nnge1  11653  zltp1le  12020  gtndiv  12047  uzss  12253  eluzadd  12261  uzm1  12264  addlelt  12491  xrre2  12551  xrre3  12552  xrmaxlt  12562  xrmaxle  12564  xrsupsslem  12688  xrub  12693  supxrunb1  12700  zltaddlt1le  12883  nn0p1elfzo  13075  elfzoext  13089  flflp1  13172  ceile  13212  modfzo0difsn  13306  seqf1olem1  13405  leexp2r  13534  expnlbnd2  13591  facavg  13657  wrdred1hash  13904  ccat2s1fvw  13989  ccat2s1fvwOLD  13990  caubnd2  14709  limsupbnd1  14831  limsupbnd2  14832  rlim2lt  14846  rlim3  14847  o1co  14935  mulcn2  14944  cn1lem  14946  rlimo1  14965  climsqz  14989  climsqz2  14990  rlimsqzlem  14997  lo1le  15000  rlimno1  15002  climsup  15018  caucvgrlem2  15023  iseraltlem2  15031  iseralt  15033  fsumabs  15148  cvgcmp  15163  cvgcmpce  15165  isumltss  15195  cvgrat  15231  ruclem9  15583  ruclem12  15586  bitsfzolem  15773  bitsfzo  15774  sadcaddlem  15796  gcdzeq  15892  algcvgblem  15911  algcvga  15913  lcmdvdsb  15947  lcmftp  15970  coprm  16045  eulerthlem2  16109  pclem  16165  infpn2  16239  prmreclem1  16242  prmreclem4  16245  ramtlecl  16326  prmgaplem7  16383  initoeu2  17268  lubval  17586  lublecllem  17590  glbval  17599  joinle  17616  latmlem1  17683  odmulg  18675  efginvrel2  18845  pgpfac1lem5  19194  chfacfscmul0  21463  chfacfpmmul0  21467  1stccnp  22067  qustgplem  22726  imasdsf1olem  22980  bldisj  23005  xbln0  23021  prdsbl  23098  metss2lem  23118  stdbdxmet  23122  ngptgp  23242  nghmcn  23351  icoopnst  23544  iocopnst  23545  cnllycmp  23561  iscau3  23882  cmetcaulem  23892  iscmet3lem1  23895  bcthlem4  23931  ovollb2lem  24092  ovolicc2lem3  24123  voliunlem3  24156  volcn  24210  itg10a  24314  itg1ge0a  24315  bddiblnc  24445  dvcnvrelem1  24620  dvfsumrlim  24634  itgsubst  24652  ulmcn  24994  ulmdvlem3  24997  mtest  24999  tanord  25130  emcllem6  25586  ftalem2  25659  chtub  25796  fsumvma2  25798  vmasum  25800  chpchtsum  25803  bcmono  25861  bclbnd  25864  bposlem1  25868  bposlem5  25872  bposlem6  25873  lgsne0  25919  gausslemma2dlem1a  25949  chtppilim  26059  dchrisumlem3  26075  pntrsumbnd2  26151  pntlemf  26189  pntlem3  26193  pntleml  26195  upgr2pthnlp  27521  crctcshwlkn0lem3  27598  crctcshwlkn0lem5  27600  eupth2lems  28023  grpoidinvlem3  28289  grpoideu  28292  vacn  28477  blocni  28588  ubthlem2  28654  chscllem2  29421  lnconi  29816  pjnmopi  29931  atomli  30165  sumdmdlem2  30202  cdj3lem2b  30220  xraddge02  30506  fedgmullem1  31113  dfon2lem5  33145  dfon2lem6  33146  nosupno  33316  cgrcoml  33570  btwnconn2  33676  fvineqsneq  34829  pibt2  34834  ltflcei  35045  poimirlem2  35059  poimirlem18  35075  poimirlem22  35079  poimirlem23  35080  poimirlem26  35083  poimirlem29  35086  poimirlem30  35087  poimirlem32  35089  heicant  35092  mblfinlem3  35096  mblfinlem4  35097  itg2addnclem  35108  itg2addnc  35111  ftc1anclem6  35135  ftc1anc  35138  mettrifi  35195  geomcau  35197  equivbnd  35228  heibor1lem  35247  bfplem1  35260  bfplem2  35261  rrncmslem  35270  divrngidl  35466  lecmtN  36552  cvrletrN  36569  llnnleat  36809  lplnnle2at  36837  lvolnle3at  36878  dalem21  36990  cdlemblem  37089  osumcllem11N  37262  pexmidlem8N  37273  lhpmcvr4N  37322  cdleme32b  37738  cdleme35fnpq  37745  cdleme48bw  37798  cdlemf1  37857  cdlemg2fv2  37896  cdlemg7fvbwN  37903  cdlemg27b  37992  tendoeq2  38070  dia2dimlem1  38360  dihord6apre  38552  dihord5apre  38558  dihglbcpreN  38596  dochnel2  38688  dihjat1lem  38724  dochexmidlem8  38763  mapdordlem2  38933  3cubeslem1  39623  iscard5  40240  frege124d  40460  mnringmulrcld  40934  climinf  42246  2ffzoeq  43883  iccpartlt  43939  lighneallem2  44122  bgoldbtbndlem3  44323  bgoldbtbndlem4  44324  tgoldbach  44333  fllog2  44980  dignn0ldlem  45014
  Copyright terms: Public domain W3C validator