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

Theorem mpand 691
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 466 . 2 (𝜑 → ((𝜒𝜓) → 𝜃))
41, 3mpan2d 690 1 (𝜑 → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  mpani  692  mp2and  695  ecase2d  1023  disjss3  5057  sotri2  5983  fpropnf1  7016  ovig  7285  orduniorsuc  7533  omopth2  8200  frfi  8752  ordunifi  8757  finsschain  8820  cantnfp1lem3  9132  cantnfp1  9133  p1le  11474  nnge1  11654  zltp1le  12021  gtndiv  12048  uzss  12254  eluzadd  12262  uzm1  12265  addlelt  12493  xrre2  12553  xrre3  12554  xrmaxlt  12564  xrmaxle  12566  xrsupsslem  12690  xrub  12695  supxrunb1  12702  zltaddlt1le  12880  nn0p1elfzo  13070  elfzoext  13084  flflp1  13167  ceile  13207  modfzo0difsn  13301  seqf1olem1  13399  leexp2r  13528  expnlbnd2  13585  facavg  13651  wrdred1hash  13903  ccat2s1fvw  13988  ccat2s1fvwOLD  13989  caubnd2  14707  limsupbnd1  14829  limsupbnd2  14830  rlim2lt  14844  rlim3  14845  o1co  14933  mulcn2  14942  cn1lem  14944  rlimo1  14963  climsqz  14987  climsqz2  14988  rlimsqzlem  14995  lo1le  14998  rlimno1  15000  climsup  15016  caucvgrlem2  15021  iseraltlem2  15029  iseralt  15031  fsumabs  15146  cvgcmp  15161  cvgcmpce  15163  isumltss  15193  cvgrat  15229  ruclem9  15581  ruclem12  15584  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  17266  lubval  17584  lublecllem  17588  glbval  17597  joinle  17614  latmlem1  17681  odmulg  18614  efginvrel2  18784  pgpfac1lem5  19132  chfacfscmul0  21396  chfacfpmmul0  21400  1stccnp  22000  qustgplem  22658  imasdsf1olem  22912  bldisj  22937  xbln0  22953  prdsbl  23030  metss2lem  23050  stdbdxmet  23054  ngptgp  23174  nghmcn  23283  icoopnst  23472  iocopnst  23473  cnllycmp  23489  iscau3  23810  cmetcaulem  23820  iscmet3lem1  23823  bcthlem4  23859  ovollb2lem  24018  ovolicc2lem3  24049  voliunlem3  24082  volcn  24136  itg10a  24240  itg1ge0a  24241  dvcnvrelem1  24543  dvfsumrlim  24557  itgsubst  24575  ulmcn  24916  ulmdvlem3  24919  mtest  24921  tanord  25049  emcllem6  25506  ftalem2  25579  chtub  25716  fsumvma2  25718  vmasum  25720  chpchtsum  25723  bcmono  25781  bclbnd  25784  bposlem1  25788  bposlem5  25792  bposlem6  25793  lgsne0  25839  gausslemma2dlem1a  25869  chtppilim  25979  dchrisumlem3  25995  pntrsumbnd2  26071  pntlemf  26109  pntlem3  26113  pntleml  26115  upgr2pthnlp  27441  crctcshwlkn0lem3  27518  crctcshwlkn0lem5  27520  eupth2lems  27945  grpoidinvlem3  28211  grpoideu  28214  vacn  28399  blocni  28510  ubthlem2  28576  chscllem2  29343  lnconi  29738  pjnmopi  29853  atomli  30087  sumdmdlem2  30124  cdj3lem2b  30142  xraddge02  30407  fedgmullem1  30925  dfon2lem5  32930  dfon2lem6  32931  nosupno  33101  cgrcoml  33355  btwnconn2  33461  fvineqsneq  34576  pibt2  34581  ltflcei  34762  poimirlem2  34776  poimirlem18  34792  poimirlem22  34796  poimirlem23  34797  poimirlem26  34800  poimirlem29  34803  poimirlem30  34804  poimirlem32  34806  heicant  34809  mblfinlem3  34813  mblfinlem4  34814  itg2addnclem  34825  itg2addnc  34828  bddiblnc  34844  ftc1anclem6  34854  ftc1anc  34857  mettrifi  34915  geomcau  34917  equivbnd  34951  heibor1lem  34970  bfplem1  34983  bfplem2  34984  rrncmslem  34993  divrngidl  35189  lecmtN  36274  cvrletrN  36291  llnnleat  36531  lplnnle2at  36559  lvolnle3at  36600  dalem21  36712  cdlemblem  36811  osumcllem11N  36984  pexmidlem8N  36995  lhpmcvr4N  37044  cdleme32b  37460  cdleme35fnpq  37467  cdleme48bw  37520  cdlemf1  37579  cdlemg2fv2  37618  cdlemg7fvbwN  37625  cdlemg27b  37714  tendoeq2  37792  dia2dimlem1  38082  dihord6apre  38274  dihord5apre  38280  dihglbcpreN  38318  dochnel2  38410  dihjat1lem  38446  dochexmidlem8  38485  mapdordlem2  38655  3cubeslem1  39161  iscard5  39781  frege124d  39986  climinf  41767  2ffzoeq  43409  iccpartlt  43431  lighneallem2  43618  bgoldbtbndlem3  43819  bgoldbtbndlem4  43820  tgoldbach  43829  fllog2  44526  dignn0ldlem  44560
  Copyright terms: Public domain W3C validator