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  5056  sotri2  5982  fpropnf1  7016  ovig  7285  orduniorsuc  7534  omopth2  8199  frfi  8751  ordunifi  8756  finsschain  8819  cantnfp1lem3  9131  cantnfp1  9132  p1le  11473  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  12878  nn0p1elfzo  13068  elfzoext  13082  flflp1  13165  ceile  13205  modfzo0difsn  13299  seqf1olem1  13397  leexp2r  13526  expnlbnd2  13583  facavg  13649  wrdred1hash  13901  ccat2s1fvw  13986  ccat2s1fvwOLD  13987  caubnd2  14705  limsupbnd1  14827  limsupbnd2  14828  rlim2lt  14842  rlim3  14843  o1co  14931  mulcn2  14940  cn1lem  14942  rlimo1  14961  climsqz  14985  climsqz2  14986  rlimsqzlem  14993  lo1le  14996  rlimno1  14998  climsup  15014  caucvgrlem2  15019  iseraltlem2  15027  iseralt  15029  fsumabs  15144  cvgcmp  15159  cvgcmpce  15161  isumltss  15191  cvgrat  15227  ruclem9  15579  ruclem12  15582  bitsfzolem  15771  bitsfzo  15772  sadcaddlem  15794  gcdzeq  15890  algcvgblem  15909  algcvga  15911  lcmdvdsb  15945  lcmftp  15968  coprm  16043  eulerthlem2  16107  pclem  16163  infpn2  16237  prmreclem1  16240  prmreclem4  16243  ramtlecl  16324  prmgaplem7  16381  initoeu2  17264  lubval  17582  lublecllem  17586  glbval  17595  joinle  17612  latmlem1  17679  odmulg  18612  efginvrel2  18782  pgpfac1lem5  19130  chfacfscmul0  21394  chfacfpmmul0  21398  1stccnp  21998  qustgplem  22656  imasdsf1olem  22910  bldisj  22935  xbln0  22951  prdsbl  23028  metss2lem  23048  stdbdxmet  23052  ngptgp  23172  nghmcn  23281  icoopnst  23470  iocopnst  23471  cnllycmp  23487  iscau3  23808  cmetcaulem  23818  iscmet3lem1  23821  bcthlem4  23857  ovollb2lem  24016  ovolicc2lem3  24047  voliunlem3  24080  volcn  24134  itg10a  24238  itg1ge0a  24239  dvcnvrelem1  24541  dvfsumrlim  24555  itgsubst  24573  ulmcn  24914  ulmdvlem3  24917  mtest  24919  tanord  25049  emcllem6  25505  ftalem2  25578  chtub  25715  fsumvma2  25717  vmasum  25719  chpchtsum  25722  bcmono  25780  bclbnd  25783  bposlem1  25787  bposlem5  25791  bposlem6  25792  lgsne0  25838  gausslemma2dlem1a  25868  chtppilim  25978  dchrisumlem3  25994  pntrsumbnd2  26070  pntlemf  26108  pntlem3  26112  pntleml  26114  upgr2pthnlp  27440  crctcshwlkn0lem3  27517  crctcshwlkn0lem5  27519  eupth2lems  27944  grpoidinvlem3  28210  grpoideu  28213  vacn  28398  blocni  28509  ubthlem2  28575  chscllem2  29342  lnconi  29737  pjnmopi  29852  atomli  30086  sumdmdlem2  30123  cdj3lem2b  30141  xraddge02  30406  fedgmullem1  30924  dfon2lem5  32929  dfon2lem6  32930  nosupno  33100  cgrcoml  33354  btwnconn2  33460  fvineqsneq  34575  pibt2  34580  ltflcei  34761  poimirlem2  34775  poimirlem18  34791  poimirlem22  34795  poimirlem23  34796  poimirlem26  34799  poimirlem29  34802  poimirlem30  34803  poimirlem32  34805  heicant  34808  mblfinlem3  34812  mblfinlem4  34813  itg2addnclem  34824  itg2addnc  34827  bddiblnc  34843  ftc1anclem6  34853  ftc1anc  34856  mettrifi  34913  geomcau  34915  equivbnd  34949  heibor1lem  34968  bfplem1  34981  bfplem2  34982  rrncmslem  34991  divrngidl  35187  lecmtN  36272  cvrletrN  36289  llnnleat  36529  lplnnle2at  36557  lvolnle3at  36598  dalem21  36710  cdlemblem  36809  osumcllem11N  36982  pexmidlem8N  36993  lhpmcvr4N  37042  cdleme32b  37458  cdleme35fnpq  37465  cdleme48bw  37518  cdlemf1  37577  cdlemg2fv2  37616  cdlemg7fvbwN  37623  cdlemg27b  37712  tendoeq2  37790  dia2dimlem1  38080  dihord6apre  38272  dihord5apre  38278  dihglbcpreN  38316  dochnel2  38408  dihjat1lem  38444  dochexmidlem8  38483  mapdordlem2  38653  3cubeslem1  39159  iscard5  39779  frege124d  39984  climinf  41763  2ffzoeq  43405  iccpartlt  43461  lighneallem2  43648  bgoldbtbndlem3  43849  bgoldbtbndlem4  43850  tgoldbach  43859  fllog2  44556  dignn0ldlem  44590
  Copyright terms: Public domain W3C validator