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

Theorem mp2and 695
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 691 . 2 (𝜑 → (𝜒𝜃))
51, 4mpd 15 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:  reu2eqd  3724  ssnelpssd  4086  tfisi  7562  tfindsg2  7565  mposn  7787  smoord  7991  oelimcl  8215  oeeui  8217  nnawordex  8252  omabs  8263  ertrd  8294  omxpenlem  8606  ixpfi2  8810  oismo  8992  cantnflem1c  9138  cantnflem1  9140  cantnflem3  9142  infxpenc2  9436  isfin2-2  9729  axdc2lem  9858  r1limwun  10146  letrd  10785  lelttrd  10786  ltletrd  10788  lttrd  10789  le2addd  11247  le2subd  11248  ltleaddd  11249  leltaddd  11250  lt2subd  11252  ltmul12a  11484  lemul12ad  11570  lemul12bd  11571  lt2halvesd  11873  uzind  12062  uztrn  12249  xrlttrd  12540  xrlelttrd  12541  xrltletrd  12542  xrletrd  12543  supxrunb1  12700  supxrunb2  12701  ixxun  12742  ixxss1  12744  ixxss2  12745  ixxss12  12746  fldiv4p1lem1div2  13193  fldiv4lem1div2uz2  13194  seqf1o  13399  faclbnd3  13640  rtrclreclem3  14407  relexpindlem  14410  sqrlem1  14590  sqrlem4  14593  sqrlem7  14596  abs3lemd  14809  rlimcn2  14935  o1of2  14957  lo1add  14971  lo1mul  14972  modfsummod  15137  mertenslem1  15228  sin01gt0  15531  cos01gt0  15532  sin02gt0  15533  dvds2subd  15633  bitsmod  15773  sadaddlem  15803  bezoutlem4  15878  mulgcd  15884  gcddvdslcm  15934  lcmgcdeq  15944  lcmfunsnlem2lem2  15971  mulgcddvds  15987  rpmulgcd2  15988  rpdvds  15992  divgcdcoprmex  15998  isprm5  16039  rpexp  16052  phimullem  16104  eulerthlem1  16106  eulerthlem2  16107  prmdiveq  16111  pythagtriplem4  16144  pcpremul  16168  pcqmul  16178  pcdvdstr  16200  pcgcd1  16201  pcadd  16213  pockthlem  16229  prmreclem2  16241  4sqlem8  16269  4sqlem14  16282  4sqlem16  16284  ramub1lem1  16350  ramub1lem2  16351  prmdvdsprmop  16367  prmgaplem1  16373  prmgaplcmlem1  16375  prmgaplem7  16381  iscatd2  16940  cicsym  17062  initoeu2  17264  joinval  17603  meetval  17617  lattrd  17656  latledi  17687  mulgass  18202  gaorber  18376  psgnunilem4  18554  efgredlem  18802  odadd2  18898  dmdprdpr  19100  ablfacrp2  19118  ablfac1b  19121  ablfac1eu  19124  pgpfac1  19131  gsumbagdiaglem  20083  znunit  20638  mdetunilem1  21149  mdetunilem4  21152  mdetunilem9  21157  neiptoptop  21667  lmcnp  21840  txcls  22140  txlly  22172  txnlly  22173  tx1stc  22186  alexsubALTlem1  22583  prdsmet  22907  blin2  22966  blcvx  23333  tgqioo  23335  metnrmlem3  23396  iscmet3lem2  23822  ovolmge0  24005  ovolunlem2  24026  mbfi1flimlem  24250  mbfmullem  24253  itg2add  24287  dvferm1lem  24508  dvferm2lem  24510  dvlip2  24519  dvge0  24530  dvcvx  24544  dvfsumabs  24547  ftc1a  24561  plyadd  24734  plymul  24735  dgrlb  24753  plydivlem4  24812  vieta1lem2  24827  ulmdvlem3  24917  sinq12gt0  25020  logdivlti  25130  fsumharmonic  25516  fsumdvdsdiaglem  25687  dvdsmulf1o  25698  logfacubnd  25724  perfectlem1  25732  dchrptlem2  25768  lgsmod  25826  2sqlem3  25923  2sqlem5  25925  2sqlem8  25929  2sqmod  25939  dchrisum0flblem2  26012  pntibndlem2  26094  pntlemr  26105  pntlemp  26113  axtgpasch  26180  tgjustr  26187  wlkcompim  27340  wwlksnredwwlkn  27600  wwlksnextsurj  27605  upgr4cycl4dv4e  27891  ex-natded5.2-2  28111  chscllem2  29342  chscllem4  29344  nmopge0  29615  nmfnge0  29631  nmoptrii  29798  staddi  29950  stadd3i  29952  atcvatlem  30089  supssd  30371  infssd  30372  xrofsup  30418  xrge0addgt0  30605  archiabllem2c  30751  orngmul  30803  linds2eq  30868  lbsdiflsp0  30921  fedgmullem2  30925  esumpmono  31237  unelldsys  31316  omssubaddlem  31456  signstfvneq0  31741  axtgupdim2ALTV  31838  bnj1098  31954  bnj1110  32151  bnj1121  32154  0nn0m1nnn0  32248  cplgredgex  32264  erdszelem8  32342  txsconn  32385  cvmlift2lem10  32456  cvmlift3lem7  32469  dvdspw  32879  sotrd  32898  dfon2lem6  32930  dfon2lem8  32932  frpomin  32975  nosupbnd1  33111  nosupbnd2lem1  33112  nosupbnd2  33113  noetalem3  33116  slttrd  33135  sltletrd  33136  slelttrd  33137  sletrd  33138  cgrtr4d  33343  cgrtrand  33351  cgrtr3and  33353  cgrextendand  33367  btwnexch3and  33379  btwnexchand  33384  linecgrand  33440  endofsegidand  33444  btwnconn1lem4  33448  btwnconn1lem8  33452  btwnconn1lem11  33455  btwnconn1lem12  33456  brsegle2  33467  seglecgr12im  33468  segleantisym  33473  colinbtwnle  33476  broutsideof2  33480  outsideoftr  33487  outsidele  33490  lineelsb2  33506  linethru  33511  gtinf  33564  copsex2d  34323  relowlssretop  34526  pibt2  34580  heicant  34808  mbfresfi  34819  ftc1anclem6  34853  eqvreltrd  35723  riotasv2d  35973  lcvnbtwn2  36043  lcvnbtwn3  36044  lcvexchlem4  36053  omlfh1N  36274  atlen0  36326  atlatmstc  36335  cvratlem  36437  lnnat  36443  2atlt  36455  athgt  36472  1cvratex  36489  ps-2  36494  llncmp  36538  llncvrlpln  36574  lplncmp  36578  lplncvrlvol  36632  lvolcmp  36633  dalemcea  36676  dalem-cly  36687  dalem10  36689  dalem17  36696  dalem25  36714  dalem38  36726  dalem44  36732  dalem55  36743  2atm2atN  36801  cdlema1N  36807  paddasslem5  36840  dalawlem3  36889  dalawlem7  36893  dalawlem11  36897  dalawlem12  36898  lhp0lt  37019  4atexlemc  37085  cdlemg33a  37722  cdlemg33  37727  cdlemk51  37969  dia2dimlem2  38081  dia2dimlem3  38082  dihmeetlem20N  38342  ismrcd2  39174  pellqrex  39354  jm2.17b  39436  dvdsacongtr  39459  jm2.26lem3  39476  jm2.27a  39480  jm2.27c  39482  fnwe2lem2  39529  addrcom  40684  infxrunb2  41512  0ellimcdiv  41806  stoweidlem15  42177  stoweidlem26  42188  stoweidlem28  42190  stoweidlem32  42194  stoweidlem44  42206  meadjuni  42616  dfatcolem  43331  icceuelpart  43473  perfectALTVlem1  43763  bgoldbtbndlem2  43848  bgoldbtbndlem3  43849  copisnmnd  43953  symgsubmefmndALT  43996  assintopass  44049  lcoss  44419  islindeps2  44466  isldepslvec2  44468  difmodm1lt  44510
  Copyright terms: Public domain W3C validator