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

Theorem mp2and 715
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 711 . 2 (𝜑 → (𝜒𝜃))
51, 4mpd 15 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  reu2eqd  3436  ssnelpssd  3752  tfisi  7100  tfindsg2  7103  mpt2sn  7313  smoord  7507  oelimcl  7725  oeeui  7727  nnawordex  7762  omabs  7772  ertrd  7803  omxpenlem  8102  ixpfi2  8305  oismo  8486  cantnflem1c  8622  cantnflem1  8624  cantnflem3  8626  infxpenc2  8883  axdc2lem  9308  r1limwun  9596  letrd  10232  lelttrd  10233  ltletrd  10235  lttrd  10236  le2addd  10684  le2subd  10685  ltleaddd  10686  leltaddd  10687  lt2subd  10689  ltmul12a  10917  lemul12ad  11004  lemul12bd  11005  lt2halvesd  11318  uzind  11507  uztrn  11742  xrlttrd  12028  xrlelttrd  12029  xrltletrd  12030  xrletrd  12031  supxrunb1  12187  supxrunb2  12188  ixxun  12229  ixxss1  12231  ixxss2  12232  ixxss12  12233  fldiv4p1lem1div2  12676  fldiv4lem1div2uz2  12677  seqf1o  12882  faclbnd3  13119  rtrclreclem3  13844  sqrlem1  14027  sqrlem4  14030  sqrlem7  14033  abs3lemd  14244  rlimcn2  14365  o1of2  14387  lo1add  14401  lo1mul  14402  modfsummod  14570  mertenslem1  14660  sin01gt0  14964  cos01gt0  14965  sin02gt0  14966  dvds2subd  15064  bitsmod  15205  sadaddlem  15235  bezoutlem4  15306  mulgcd  15312  gcddvdslcm  15362  lcmgcdeq  15372  lcmfunsnlem2lem2  15399  mulgcddvds  15416  rpmulgcd2  15417  rpdvds  15421  divgcdcoprmex  15427  isprm5  15466  rpexp  15479  phimullem  15531  eulerthlem1  15533  eulerthlem2  15534  prmdiv  15537  prmdiveq  15538  pythagtriplem4  15571  pcpremul  15595  pcqmul  15605  pcdvdstr  15627  pcgcd1  15628  pcadd  15640  pockthlem  15656  prmreclem2  15668  4sqlem8  15696  4sqlem10  15698  4sqlem14  15709  4sqlem16  15711  ramub1lem1  15777  ramub1lem2  15778  prmdvdsprmop  15794  prmgaplem1  15800  prmgaplcmlem1  15802  prmgaplem7  15808  iscatd2  16389  cicsym  16511  initoeu2  16713  joinval  17052  meetval  17066  lattrd  17105  latledi  17136  mulgass  17626  gaorber  17787  psgnunilem4  17963  efgredlem  18206  odadd2  18298  dmdprdpr  18494  ablfacrp2  18512  ablfac1b  18515  ablfac1eu  18518  pgpfac1  18525  gsumbagdiaglem  19423  znunit  19960  mdetunilem1  20466  mdetunilem4  20469  mdetunilem9  20474  neiptoptop  20983  lmcnp  21156  txcls  21455  txlly  21487  txnlly  21488  tx1stc  21501  alexsubALTlem1  21898  prdsmet  22222  blin2  22281  blcvx  22648  tgqioo  22650  metnrmlem3  22711  iscmet3lem2  23136  ovolmge0  23291  ovolunlem2  23312  mbfi1flimlem  23534  mbfmullem  23537  itg2add  23571  dvlip2  23803  dvge0  23814  dvcvx  23828  dvfsumabs  23831  plyadd  24018  plymul  24019  dgrlb  24037  plydivlem4  24096  vieta1lem2  24111  ulmdvlem3  24201  sinq12gt0  24304  logdivlti  24411  fsumharmonic  24783  fsumdvdsdiaglem  24954  dvdsmulf1o  24965  logfacubnd  24991  perfectlem1  24999  dchrptlem2  25035  lgsmod  25093  2sqlem3  25190  2sqlem5  25192  2sqlem8  25196  dchrisum0flblem2  25243  pntibndlem2  25325  pntlemr  25336  pntlemp  25344  axtgpasch  25411  wlkcompim  26583  wwlksnredwwlkn  26858  wwlksnextsur  26863  upgr4cycl4dv4e  27163  ex-natded5.2-2  27392  chscllem2  28625  chscllem4  28627  nmopge0  28898  nmfnge0  28914  nmoptrii  29081  staddi  29233  stadd3i  29235  atcvatlem  29372  supssd  29615  infssd  29616  xrofsup  29661  2sqmod  29776  xrge0addgt0  29819  archiabllem2c  29877  orngmul  29931  esumpmono  30269  unelldsys  30349  omssubaddlem  30489  signstfvneq0  30777  axtgupdim2OLD  30874  bnj1098  30980  bnj1110  31176  bnj1121  31179  erdszelem8  31306  txsconn  31349  cvmlift2lem10  31420  cvmlift3lem7  31433  dvdspw  31762  sotrd  31781  dfon2lem6  31817  dfon2lem8  31819  frpomin  31863  nosupbnd1  31985  nosupbnd2lem1  31986  nosupbnd2  31987  noetalem3  31990  slttrd  32009  sltletrd  32010  slelttrd  32011  sletrd  32012  cgrtr4d  32217  cgrtrand  32225  cgrtr3and  32227  cgrextendand  32241  btwnexch3and  32253  btwnexchand  32258  linecgrand  32314  endofsegidand  32318  btwnconn1lem4  32322  btwnconn1lem8  32326  btwnconn1lem11  32329  btwnconn1lem12  32330  brsegle2  32341  seglecgr12im  32342  segleantisym  32347  colinbtwnle  32350  broutsideof2  32354  outsideoftr  32361  outsidele  32364  lineelsb2  32380  linethru  32385  gtinf  32438  gtinfOLD  32439  relowlssretop  33341  heicant  33574  mbfresfi  33586  ftc1anclem6  33620  riotasv2d  34561  lcvnbtwn2  34632  lcvnbtwn3  34633  lcvexchlem4  34642  omlfh1N  34863  atlen0  34915  atlatmstc  34924  cvratlem  35025  lnnat  35031  2atlt  35043  athgt  35060  1cvratex  35077  ps-2  35082  llncmp  35126  llncvrlpln  35162  lplncmp  35166  lplncvrlvol  35220  lvolcmp  35221  dalemcea  35264  dalem-cly  35275  dalem10  35277  dalem17  35284  dalem25  35302  dalem38  35314  dalem44  35320  dalem55  35331  2atm2atN  35389  cdlema1N  35395  paddasslem5  35428  dalawlem3  35477  dalawlem7  35481  dalawlem11  35485  dalawlem12  35486  lhp0lt  35607  4atexlemc  35673  cdlemg33a  36311  cdlemg33  36316  cdlemk51  36558  dia2dimlem2  36671  dia2dimlem3  36672  dihmeetlem20N  36932  ismrcd2  37579  pellqrex  37760  jm2.17b  37845  dvdsacongtr  37868  jm2.26lem3  37885  jm2.27a  37889  jm2.27c  37891  fnwe2lem2  37938  fco2d  38778  addrcom  38996  infxrunb2  39897  0ellimcdiv  40199  stoweidlem15  40550  stoweidlem26  40561  stoweidlem28  40563  stoweidlem32  40567  stoweidlem44  40579  icceuelpart  41697  perfectALTVlem1  41955  bgoldbtbndlem2  42019  bgoldbtbndlem3  42020  copisnmnd  42134  assintopass  42175  lcoss  42550  islindeps2  42597  isldepslvec2  42599  difmodm1lt  42642
  Copyright terms: Public domain W3C validator