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

Theorem mpand 711
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 710 1 (𝜑 → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  mpani  712  mp2and  715  ecase2d  1000  disjss3  4684  sotri2  5560  fpropnf1  6564  ovig  6824  orduniorsuc  7072  omopth2  7709  frfi  8246  ordunifi  8251  finsschain  8314  cantnfp1lem3  8615  cantnfp1  8616  p1le  10904  nnge1  11084  zltp1le  11465  gtndiv  11492  uzss  11746  eluzadd  11754  uzm1  11756  addlelt  11980  xrre2  12039  xrre3  12040  xrmaxlt  12050  xrmaxle  12052  xrsupsslem  12175  xrub  12180  supxrunb1  12187  zltaddlt1le  12362  nn0p1elfzo  12550  elfzoext  12564  flflp1  12648  ceile  12688  modfzo0difsn  12782  seqf1olem1  12880  leexp2r  12958  expnlbnd2  13035  facavg  13128  wrdred1hash  13383  ccat2s1fvw  13460  caubnd2  14141  limsupbnd1  14257  limsupbnd2  14258  rlim2lt  14272  rlim3  14273  o1co  14361  mulcn2  14370  cn1lem  14372  rlimo1  14391  climsqz  14415  climsqz2  14416  rlimsqzlem  14423  lo1le  14426  rlimno1  14428  climsup  14444  caucvgrlem2  14449  iseraltlem2  14457  iseralt  14459  fsumabs  14577  cvgcmp  14592  cvgcmpce  14594  isumltss  14624  cvgrat  14659  ruclem9  15011  ruclem12  15014  bitsfzolem  15203  bitsfzo  15204  sadcaddlem  15226  gcdzeq  15318  algcvgblem  15337  algcvga  15339  lcmdvdsb  15373  lcmftp  15396  coprmdvdsOLD  15414  coprm  15470  eulerthlem2  15534  pclem  15590  infpn2  15664  prmreclem1  15667  prmreclem4  15670  ramtlecl  15751  prmgaplem7  15808  initoeu2  16713  lubval  17031  lublecllem  17035  glbval  17044  joinle  17061  latmlem1  17128  odmulg  18019  efginvrel2  18186  pgpfac1lem5  18524  chfacfscmul0  20711  chfacfpmmul0  20715  1stccnp  21313  qustgplem  21971  imasdsf1olem  22225  bldisj  22250  xbln0  22266  prdsbl  22343  metss2lem  22363  stdbdxmet  22367  ngptgp  22487  nghmcn  22596  icoopnst  22785  iocopnst  22786  cnllycmp  22802  iscau3  23122  cmetcaulem  23132  iscmet3lem1  23135  bcthlem4  23170  ovollb2lem  23302  ovolicc2lem3  23333  voliunlem3  23366  volcn  23420  itg10a  23522  itg1ge0a  23523  dvcnvrelem1  23825  dvfsumrlim  23839  itgsubst  23857  ulmcn  24198  ulmdvlem3  24201  mtest  24203  tanord  24329  emcllem6  24772  ftalem2  24845  chtub  24982  fsumvma2  24984  vmasum  24986  chpchtsum  24989  bcmono  25047  bclbnd  25050  bposlem1  25054  bposlem5  25058  bposlem6  25059  lgsne0  25105  gausslemma2dlem1a  25135  chtppilim  25209  dchrisumlem3  25225  pntrsumbnd2  25301  pntlemf  25339  pntlem3  25343  pntleml  25345  upgr2pthnlp  26684  crctcshwlkn0lem3  26760  crctcshwlkn0lem5  26762  eupth2lems  27216  grpoidinvlem3  27488  grpoideu  27491  vacn  27677  blocni  27788  ubthlem2  27855  chscllem2  28625  lnconi  29020  pjnmopi  29135  atomli  29369  sumdmdlem2  29406  cdj3lem2b  29424  xraddge02  29649  dfon2lem5  31816  dfon2lem6  31817  nosupno  31974  cgrcoml  32228  btwnconn2  32334  ltflcei  33527  poimirlem2  33541  poimirlem18  33557  poimirlem22  33561  poimirlem23  33562  poimirlem26  33565  poimirlem29  33568  poimirlem30  33569  poimirlem32  33571  heicant  33574  mblfinlem3  33578  mblfinlem4  33579  itg2addnclem  33591  itg2addnc  33594  bddiblnc  33610  ftc1anclem6  33620  ftc1anc  33623  mettrifi  33683  geomcau  33685  equivbnd  33719  heibor1lem  33738  bfplem1  33751  bfplem2  33752  rrncmslem  33761  divrngidl  33957  lecmtN  34861  cvrletrN  34878  llnnleat  35117  lplnnle2at  35145  lvolnle3at  35186  dalem21  35298  cdlemblem  35397  osumcllem11N  35570  pexmidlem8N  35581  lhpmcvr4N  35630  cdleme32b  36047  cdleme35fnpq  36054  cdleme48bw  36107  cdlemf1  36166  cdlemg2fv2  36205  cdlemg7fvbwN  36212  cdlemg27b  36301  tendoeq2  36379  dia2dimlem1  36670  dihord6apre  36862  dihord5apre  36868  dihglbcpreN  36906  dochnel2  36998  dihjat1lem  37034  dochexmidlem8  37073  mapdordlem2  37243  frege124d  38370  climinf  40156  2ffzoeq  41663  iccpartlt  41685  lighneallem2  41848  bgoldbtbndlem3  42020  bgoldbtbndlem4  42021  tgoldbach  42030  tgoldbachOLD  42037  fllog2  42687  dignn0ldlem  42721
  Copyright terms: Public domain W3C validator