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

Theorem mp2and 710
Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
Hypotheses
Ref Expression
mp2and.1 (𝜑𝜓)
mp2and.2 (𝜑𝜒)
mp2and.3 (𝜑 → ((𝜓𝜒) → 𝜃))
Assertion
Ref Expression
mp2and (𝜑𝜃)

Proof of Theorem mp2and
StepHypRef Expression
1 mp2and.2 . 2 (𝜑𝜒)
2 mp2and.1 . . 3 (𝜑𝜓)
3 mp2and.3 . . 3 (𝜑 → ((𝜓𝜒) → 𝜃))
42, 3mpand 706 . 2 (𝜑 → (𝜒𝜃))
51, 4mpd 15 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  reu2eqd  3369  ssnelpssd  3680  tfisi  6927  tfindsg2  6930  mpt2sn  7132  smoord  7326  oelimcl  7544  oeeui  7546  nnawordex  7581  omabs  7591  ertrd  7622  omxpenlem  7923  ixpfi2  8124  oismo  8305  cantnflem1c  8444  cantnflem1  8446  cantnflem3  8448  infxpenc2  8705  axdc2lem  9130  r1limwun  9414  letrd  10045  lelttrd  10046  ltletrd  10048  lttrd  10049  le2addd  10495  le2subd  10496  ltleaddd  10497  leltaddd  10498  lt2subd  10500  ltmul12a  10728  lemul12ad  10815  lemul12bd  10816  lt2halvesd  11127  uzind  11301  uztrn  11536  xrlttrd  11825  xrlelttrd  11826  xrltletrd  11827  xrletrd  11828  supxrunb1  11977  supxrunb2  11978  ixxun  12018  ixxss1  12020  ixxss2  12021  ixxss12  12022  fldiv4p1lem1div2  12453  fldiv4lem1div2uz2  12454  seqf1o  12659  faclbnd3  12896  rtrclreclem3  13594  sqrlem1  13777  sqrlem4  13780  sqrlem7  13783  abs3lemd  13994  rlimcn2  14115  o1of2  14137  lo1add  14151  lo1mul  14152  modfsummod  14313  mertenslem1  14401  sin01gt0  14705  cos01gt0  14706  sin02gt0  14707  dvds2subd  14801  bitsmod  14942  sadaddlem  14972  bezoutlem4  15043  mulgcd  15049  gcddvdslcm  15099  lcmgcdeq  15109  lcmfunsnlem2lem2  15136  mulgcddvds  15153  rpmulgcd2  15154  rpdvds  15158  divgcdcoprmex  15164  isprm5  15203  rpexp  15216  phimullem  15268  eulerthlem1  15270  eulerthlem2  15271  prmdiv  15274  prmdiveq  15275  pythagtriplem4  15308  pcpremul  15332  pcqmul  15342  pcdvdstr  15364  pcgcd1  15365  pcadd  15377  pockthlem  15393  prmreclem2  15405  4sqlem8  15433  4sqlem10  15435  4sqlem14  15446  4sqlem16  15448  ramub1lem1  15514  ramub1lem2  15515  prmdvdsprmop  15531  prmgaplem1  15537  prmgaplcmlem1  15539  prmgaplem7  15545  iscatd2  16111  cicsym  16233  initoeu2  16435  joinval  16774  meetval  16788  lattrd  16827  latledi  16858  mulgass  17348  gaorber  17510  psgnunilem4  17686  efgredlem  17929  odadd2  18021  dmdprdpr  18217  ablfacrp2  18235  ablfac1b  18238  ablfac1eu  18241  pgpfac1  18248  gsumbagdiaglem  19142  znunit  19676  mdetunilem1  20179  mdetunilem4  20182  mdetunilem9  20187  neiptoptop  20687  lmcnp  20860  txcls  21159  txlly  21191  txnlly  21192  tx1stc  21205  alexsubALTlem1  21603  prdsmet  21926  blin2  21985  blcvx  22341  tgqioo  22343  metnrmlem3  22403  iscmet3lem2  22816  ovolmge0  22969  ovolunlem2  22990  mbfi1flimlem  23212  mbfmullem  23215  itg2add  23249  dvlip2  23479  dvge0  23490  dvcvx  23504  dvfsumabs  23507  plyadd  23694  plymul  23695  dgrlb  23713  plydivlem4  23772  vieta1lem2  23787  ulmdvlem3  23877  sinq12gt0  23980  logdivlti  24087  fsumharmonic  24455  fsumdvdsdiaglem  24626  dvdsmulf1o  24637  logfacubnd  24663  perfectlem1  24671  dchrptlem2  24707  lgsmod  24765  2sqlem3  24862  2sqlem5  24864  2sqlem8  24868  dchrisum0flblem2  24915  pntibndlem2  24997  pntlemr  25008  pntlemp  25016  axtgpasch  25083  wwlknredwwlkn  26020  wwlkextsur  26025  ex-natded5.2-2  26420  chscllem2  27687  chscllem4  27689  nmopge0  27960  nmfnge0  27976  nmoptrii  28143  staddi  28295  stadd3i  28297  atcvatlem  28434  supssd  28676  infssd  28677  xrofsup  28729  2sqmod  28785  xrge0addgt0  28828  archiabllem2c  28886  orngmul  28940  esumpmono  29274  unelldsys  29354  omssubaddlem  29494  signstfvneq0  29781  axtgupdim2OLD  29805  bnj1098  29914  bnj1110  30110  bnj1121  30113  erdszelem8  30240  txscon  30283  cvmlift2lem10  30354  cvmlift3lem7  30367  dvdspw  30695  dfon2lem6  30743  dfon2lem8  30745  cgrtr4d  31068  cgrtrand  31076  cgrtr3and  31078  cgrextendand  31092  btwnexch3and  31104  btwnexchand  31109  linecgrand  31165  endofsegidand  31169  btwnconn1lem4  31173  btwnconn1lem8  31177  btwnconn1lem11  31180  btwnconn1lem12  31181  brsegle2  31192  seglecgr12im  31193  segleantisym  31198  colinbtwnle  31201  broutsideof2  31205  outsideoftr  31212  outsidele  31215  lineelsb2  31231  linethru  31236  gtinf  31289  gtinfOLD  31290  relowlssretop  32183  heicant  32410  mbfresfi  32422  ftc1anclem6  32456  riotasv2d  33057  lcvnbtwn2  33128  lcvnbtwn3  33129  lcvexchlem4  33138  omlfh1N  33359  atlen0  33411  atlatmstc  33420  cvratlem  33521  lnnat  33527  2atlt  33539  athgt  33556  1cvratex  33573  ps-2  33578  llncmp  33622  llncvrlpln  33658  lplncmp  33662  lplncvrlvol  33716  lvolcmp  33717  dalemcea  33760  dalem-cly  33771  dalem10  33773  dalem17  33780  dalem25  33798  dalem38  33810  dalem44  33816  dalem55  33827  2atm2atN  33885  cdlema1N  33891  paddasslem5  33924  dalawlem3  33973  dalawlem7  33977  dalawlem11  33981  dalawlem12  33982  lhp0lt  34103  4atexlemc  34169  cdlemg33a  34808  cdlemg33  34813  cdlemk51  35055  dia2dimlem2  35168  dia2dimlem3  35169  dihmeetlem20N  35429  ismrcd2  36076  pellqrex  36257  jm2.17b  36342  dvdsacongtr  36365  jm2.26lem3  36382  jm2.27a  36386  jm2.27c  36388  fnwe2lem2  36435  fco2d  37277  addrcom  37496  infxrunb2  38322  0ellimcdiv  38513  stoweidlem15  38705  stoweidlem26  38716  stoweidlem28  38718  stoweidlem32  38722  stoweidlem44  38734  icceuelpart  39772  perfectALTVlem1  39962  bgoldbtbndlem2  40020  bgoldbtbndlem3  40021  1wlkcompim  40831  wwlksnredwwlkn  41096  wwlksnextsur  41101  upgr4cycl4dv4e  41347  copisnmnd  41594  assintopass  41635  lcoss  42014  islindeps2  42061  isldepslvec2  42063  difmodm1lt  42106
  Copyright terms: Public domain W3C validator