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

Theorem mpand 678
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 453 . 2 (𝜑 → ((𝜒𝜓) → 𝜃))
41, 3mpan2d 677 1 (𝜑 → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  mpani  679  mp2and  682  ecase2d  1045  disjss3  4854  sotri2  5750  fpropnf1  6758  ovig  7022  orduniorsuc  7270  omopth2  7911  frfi  8454  ordunifi  8459  finsschain  8522  cantnfp1lem3  8834  cantnfp1  8835  p1le  11161  nnge1  11344  zltp1le  11713  gtndiv  11740  uzss  11945  eluzadd  11953  uzm1  11956  addlelt  12178  xrre2  12239  xrre3  12240  xrmaxlt  12250  xrmaxle  12252  xrsupsslem  12375  xrub  12380  supxrunb1  12387  zltaddlt1le  12567  nn0p1elfzo  12755  elfzoext  12769  flflp1  12852  ceile  12892  modfzo0difsn  12986  seqf1olem1  13083  leexp2r  13161  expnlbnd2  13238  facavg  13328  wrdred1hash  13582  ccat2s1fvw  13658  caubnd2  14340  limsupbnd1  14456  limsupbnd2  14457  rlim2lt  14471  rlim3  14472  o1co  14560  mulcn2  14569  cn1lem  14571  rlimo1  14590  climsqz  14614  climsqz2  14615  rlimsqzlem  14622  lo1le  14625  rlimno1  14627  climsup  14643  caucvgrlem2  14648  iseraltlem2  14656  iseralt  14658  fsumabs  14775  cvgcmp  14790  cvgcmpce  14792  isumltss  14822  cvgrat  14856  ruclem9  15207  ruclem12  15210  bitsfzolem  15395  bitsfzo  15396  sadcaddlem  15418  gcdzeq  15510  algcvgblem  15529  algcvga  15531  lcmdvdsb  15565  lcmftp  15588  coprm  15660  eulerthlem2  15724  pclem  15780  infpn2  15854  prmreclem1  15857  prmreclem4  15860  ramtlecl  15941  prmgaplem7  15998  initoeu2  16890  lubval  17209  lublecllem  17213  glbval  17222  joinle  17239  latmlem1  17306  odmulg  18194  efginvrel2  18361  pgpfac1lem5  18700  chfacfscmul0  20897  chfacfpmmul0  20901  1stccnp  21500  qustgplem  22158  imasdsf1olem  22412  bldisj  22437  xbln0  22453  prdsbl  22530  metss2lem  22550  stdbdxmet  22554  ngptgp  22674  nghmcn  22783  icoopnst  22972  iocopnst  22973  cnllycmp  22989  iscau3  23310  cmetcaulem  23320  iscmet3lem1  23323  bcthlem4  23358  ovollb2lem  23492  ovolicc2lem3  23523  voliunlem3  23556  volcn  23610  itg10a  23714  itg1ge0a  23715  dvcnvrelem1  24017  dvfsumrlim  24031  itgsubst  24049  ulmcn  24390  ulmdvlem3  24393  mtest  24395  tanord  24522  emcllem6  24964  ftalem2  25037  chtub  25174  fsumvma2  25176  vmasum  25178  chpchtsum  25181  bcmono  25239  bclbnd  25242  bposlem1  25246  bposlem5  25250  bposlem6  25251  lgsne0  25297  gausslemma2dlem1a  25327  chtppilim  25401  dchrisumlem3  25417  pntrsumbnd2  25493  pntlemf  25531  pntlem3  25535  pntleml  25537  upgr2pthnlp  26879  crctcshwlkn0lem3  26956  crctcshwlkn0lem5  26958  eupth2lems  27434  grpoidinvlem3  27712  grpoideu  27715  vacn  27900  blocni  28011  ubthlem2  28078  chscllem2  28848  lnconi  29243  pjnmopi  29358  atomli  29592  sumdmdlem2  29629  cdj3lem2b  29647  xraddge02  29871  dfon2lem5  32034  dfon2lem6  32035  nosupno  32192  cgrcoml  32446  btwnconn2  32552  ltflcei  33729  poimirlem2  33743  poimirlem18  33759  poimirlem22  33763  poimirlem23  33764  poimirlem26  33767  poimirlem29  33770  poimirlem30  33771  poimirlem32  33773  heicant  33776  mblfinlem3  33780  mblfinlem4  33781  itg2addnclem  33792  itg2addnc  33795  bddiblnc  33811  ftc1anclem6  33821  ftc1anc  33824  mettrifi  33883  geomcau  33885  equivbnd  33919  heibor1lem  33938  bfplem1  33951  bfplem2  33952  rrncmslem  33961  divrngidl  34157  lecmtN  35055  cvrletrN  35072  llnnleat  35312  lplnnle2at  35340  lvolnle3at  35381  dalem21  35493  cdlemblem  35592  osumcllem11N  35765  pexmidlem8N  35776  lhpmcvr4N  35825  cdleme32b  36241  cdleme35fnpq  36248  cdleme48bw  36301  cdlemf1  36360  cdlemg2fv2  36399  cdlemg7fvbwN  36406  cdlemg27b  36495  tendoeq2  36573  dia2dimlem1  36863  dihord6apre  37055  dihord5apre  37061  dihglbcpreN  37099  dochnel2  37191  dihjat1lem  37227  dochexmidlem8  37266  mapdordlem2  37436  frege124d  38571  climinf  40336  2ffzoeq  41931  iccpartlt  41953  lighneallem2  42116  bgoldbtbndlem3  42288  bgoldbtbndlem4  42289  tgoldbach  42298  fllog2  42948  dignn0ldlem  42982
  Copyright terms: Public domain W3C validator