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

Theorem mp2and 682
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 678 . 2 (𝜑 → (𝜒𝜃))
51, 4mpd 15 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:  reu2eqd  3601  ssnelpssd  3917  tfisi  7284  tfindsg2  7287  mpt2sn  7498  smoord  7694  oelimcl  7913  oeeui  7915  nnawordex  7950  omabs  7960  ertrd  7991  omxpenlem  8296  ixpfi2  8499  oismo  8680  cantnflem1c  8827  cantnflem1  8829  cantnflem3  8831  infxpenc2  9124  axdc2lem  9551  r1limwun  9839  letrd  10475  lelttrd  10476  ltletrd  10478  lttrd  10479  le2addd  10927  le2subd  10928  ltleaddd  10929  leltaddd  10930  lt2subd  10932  ltmul12a  11160  lemul12ad  11247  lemul12bd  11248  lt2halvesd  11543  uzind  11731  uztrn  11917  xrlttrd  12204  xrlelttrd  12205  xrltletrd  12206  xrletrd  12207  supxrunb1  12363  supxrunb2  12364  ixxun  12405  ixxss1  12407  ixxss2  12408  ixxss12  12409  fldiv4p1lem1div2  12856  fldiv4lem1div2uz2  12857  seqf1o  13061  faclbnd3  13295  rtrclreclem3  14019  sqrlem1  14202  sqrlem4  14205  sqrlem7  14208  abs3lemd  14419  rlimcn2  14540  o1of2  14562  lo1add  14576  lo1mul  14577  modfsummod  14744  mertenslem1  14833  sin01gt0  15136  cos01gt0  15137  sin02gt0  15138  dvds2subd  15236  bitsmod  15373  sadaddlem  15403  bezoutlem4  15474  mulgcd  15480  gcddvdslcm  15530  lcmgcdeq  15540  lcmfunsnlem2lem2  15567  mulgcddvds  15583  rpmulgcd2  15584  rpdvds  15588  divgcdcoprmex  15594  isprm5  15632  rpexp  15645  phimullem  15697  eulerthlem1  15699  eulerthlem2  15700  prmdiv  15703  prmdiveq  15704  pythagtriplem4  15737  pcpremul  15761  pcqmul  15771  pcdvdstr  15793  pcgcd1  15794  pcadd  15806  pockthlem  15822  prmreclem2  15834  4sqlem8  15862  4sqlem10  15864  4sqlem14  15875  4sqlem16  15877  ramub1lem1  15943  ramub1lem2  15944  prmdvdsprmop  15960  prmgaplem1  15966  prmgaplcmlem1  15968  prmgaplem7  15974  iscatd2  16542  cicsym  16664  initoeu2  16866  joinval  17206  meetval  17220  lattrd  17259  latledi  17290  mulgass  17777  gaorber  17938  psgnunilem4  18114  efgredlem  18357  odadd2  18449  dmdprdpr  18646  ablfacrp2  18664  ablfac1b  18667  ablfac1eu  18670  pgpfac1  18677  gsumbagdiaglem  19580  znunit  20115  mdetunilem1  20626  mdetunilem4  20629  mdetunilem9  20634  neiptoptop  21146  lmcnp  21319  txcls  21618  txlly  21650  txnlly  21651  tx1stc  21664  alexsubALTlem1  22061  prdsmet  22385  blin2  22444  blcvx  22811  tgqioo  22813  metnrmlem3  22874  iscmet3lem2  23300  ovolmge0  23457  ovolunlem2  23478  mbfi1flimlem  23702  mbfmullem  23705  itg2add  23739  dvlip2  23971  dvge0  23982  dvcvx  23996  dvfsumabs  23999  plyadd  24186  plymul  24187  dgrlb  24205  plydivlem4  24264  vieta1lem2  24279  ulmdvlem3  24369  sinq12gt0  24473  logdivlti  24579  fsumharmonic  24951  fsumdvdsdiaglem  25122  dvdsmulf1o  25133  logfacubnd  25159  perfectlem1  25167  dchrptlem2  25203  lgsmod  25261  2sqlem3  25358  2sqlem5  25360  2sqlem8  25364  dchrisum0flblem2  25411  pntibndlem2  25493  pntlemr  25504  pntlemp  25512  axtgpasch  25579  wlkcompim  26754  wwlksnredwwlkn  27031  wwlksnextsur  27036  upgr4cycl4dv4e  27357  ex-natded5.2-2  27592  chscllem2  28824  chscllem4  28826  nmopge0  29097  nmfnge0  29113  nmoptrii  29280  staddi  29432  stadd3i  29434  atcvatlem  29571  supssd  29813  infssd  29814  xrofsup  29859  2sqmod  29972  xrge0addgt0  30015  archiabllem2c  30073  orngmul  30127  esumpmono  30465  unelldsys  30545  omssubaddlem  30685  signstfvneq0  30973  axtgupdim2OLD  31070  bnj1098  31175  bnj1110  31371  bnj1121  31374  erdszelem8  31501  txsconn  31544  cvmlift2lem10  31615  cvmlift3lem7  31628  dvdspw  31956  sotrd  31975  dfon2lem6  32011  dfon2lem8  32013  frpomin  32057  nosupbnd1  32179  nosupbnd2lem1  32180  nosupbnd2  32181  noetalem3  32184  slttrd  32203  sltletrd  32204  slelttrd  32205  sletrd  32206  cgrtr4d  32411  cgrtrand  32419  cgrtr3and  32421  cgrextendand  32435  btwnexch3and  32447  btwnexchand  32452  linecgrand  32508  endofsegidand  32512  btwnconn1lem4  32516  btwnconn1lem8  32520  btwnconn1lem11  32523  btwnconn1lem12  32524  brsegle2  32535  seglecgr12im  32536  segleantisym  32541  colinbtwnle  32544  broutsideof2  32548  outsideoftr  32555  outsidele  32558  lineelsb2  32574  linethru  32579  gtinf  32632  gtinfOLD  32633  relowlssretop  33525  heicant  33755  mbfresfi  33766  ftc1anclem6  33800  riotasv2d  34734  lcvnbtwn2  34805  lcvnbtwn3  34806  lcvexchlem4  34815  omlfh1N  35036  atlen0  35088  atlatmstc  35097  cvratlem  35199  lnnat  35205  2atlt  35217  athgt  35234  1cvratex  35251  ps-2  35256  llncmp  35300  llncvrlpln  35336  lplncmp  35340  lplncvrlvol  35394  lvolcmp  35395  dalemcea  35438  dalem-cly  35449  dalem10  35451  dalem17  35458  dalem25  35476  dalem38  35488  dalem44  35494  dalem55  35505  2atm2atN  35563  cdlema1N  35569  paddasslem5  35602  dalawlem3  35651  dalawlem7  35655  dalawlem11  35659  dalawlem12  35660  lhp0lt  35781  4atexlemc  35847  cdlemg33a  36484  cdlemg33  36489  cdlemk51  36731  dia2dimlem2  36843  dia2dimlem3  36844  dihmeetlem20N  37104  ismrcd2  37761  pellqrex  37942  jm2.17b  38026  dvdsacongtr  38049  jm2.26lem3  38066  jm2.27a  38070  jm2.27c  38072  fnwe2lem2  38119  fco2d  38958  addrcom  39174  infxrunb2  40061  0ellimcdiv  40358  stoweidlem15  40708  stoweidlem26  40719  stoweidlem28  40721  stoweidlem32  40725  stoweidlem44  40737  dfatcolem  41841  icceuelpart  41944  perfectALTVlem1  42202  bgoldbtbndlem2  42266  bgoldbtbndlem3  42267  copisnmnd  42374  assintopass  42415  lcoss  42790  islindeps2  42837  isldepslvec2  42839  difmodm1lt  42882
  Copyright terms: Public domain W3C validator