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  3730  ssnelpssd  4092  tfisi  7564  tfindsg2  7567  mposn  7792  smoord  7996  oelimcl  8219  oeeui  8221  nnawordex  8256  omabs  8267  ertrd  8298  omxpenlem  8610  ixpfi2  8814  oismo  8996  cantnflem1c  9142  cantnflem1  9144  cantnflem3  9146  infxpenc2  9440  isfin2-2  9733  axdc2lem  9862  r1limwun  10150  letrd  10789  lelttrd  10790  ltletrd  10792  lttrd  10793  le2addd  11251  le2subd  11252  ltleaddd  11253  leltaddd  11254  lt2subd  11256  ltmul12a  11488  lemul12ad  11574  lemul12bd  11575  lt2halvesd  11877  uzind  12066  uztrn  12253  xrlttrd  12545  xrlelttrd  12546  xrltletrd  12547  xrletrd  12548  supxrunb1  12705  supxrunb2  12706  ixxun  12747  ixxss1  12749  ixxss2  12750  ixxss12  12751  fldiv4p1lem1div2  13198  fldiv4lem1div2uz2  13199  seqf1o  13404  faclbnd3  13645  rtrclreclem3  14412  relexpindlem  14415  sqrlem1  14595  sqrlem4  14598  sqrlem7  14601  abs3lemd  14814  rlimcn2  14940  o1of2  14962  lo1add  14976  lo1mul  14977  modfsummod  15141  mertenslem1  15232  sin01gt0  15535  cos01gt0  15536  sin02gt0  15537  dvds2subd  15637  bitsmod  15777  sadaddlem  15807  bezoutlem4  15882  mulgcd  15888  gcddvdslcm  15938  lcmgcdeq  15948  lcmfunsnlem2lem2  15975  mulgcddvds  15991  rpmulgcd2  15992  rpdvds  15996  divgcdcoprmex  16002  isprm5  16043  rpexp  16056  phimullem  16108  eulerthlem1  16110  eulerthlem2  16111  prmdiveq  16115  pythagtriplem4  16148  pcpremul  16172  pcqmul  16182  pcdvdstr  16204  pcgcd1  16205  pcadd  16217  pockthlem  16233  prmreclem2  16245  4sqlem8  16273  4sqlem14  16286  4sqlem16  16288  ramub1lem1  16354  ramub1lem2  16355  prmdvdsprmop  16371  prmgaplem1  16377  prmgaplcmlem1  16379  prmgaplem7  16385  iscatd2  16944  cicsym  17066  initoeu2  17268  joinval  17607  meetval  17621  lattrd  17660  latledi  17691  mulgass  18196  gaorber  18370  psgnunilem4  18547  efgredlem  18795  odadd2  18891  dmdprdpr  19093  ablfacrp2  19111  ablfac1b  19114  ablfac1eu  19117  pgpfac1  19124  gsumbagdiaglem  20076  znunit  20628  mdetunilem1  21139  mdetunilem4  21142  mdetunilem9  21147  neiptoptop  21657  lmcnp  21830  txcls  22130  txlly  22162  txnlly  22163  tx1stc  22176  alexsubALTlem1  22573  prdsmet  22897  blin2  22956  blcvx  23323  tgqioo  23325  metnrmlem3  23386  iscmet3lem2  23812  ovolmge0  23995  ovolunlem2  24016  mbfi1flimlem  24240  mbfmullem  24243  itg2add  24277  dvferm1lem  24498  dvferm2lem  24500  dvlip2  24509  dvge0  24520  dvcvx  24534  dvfsumabs  24537  ftc1a  24551  plyadd  24724  plymul  24725  dgrlb  24743  plydivlem4  24802  vieta1lem2  24817  ulmdvlem3  24907  sinq12gt0  25010  logdivlti  25118  fsumharmonic  25505  fsumdvdsdiaglem  25676  dvdsmulf1o  25687  logfacubnd  25713  perfectlem1  25721  dchrptlem2  25757  lgsmod  25815  2sqlem3  25912  2sqlem5  25914  2sqlem8  25918  2sqmod  25928  dchrisum0flblem2  26001  pntibndlem2  26083  pntlemr  26094  pntlemp  26102  axtgpasch  26169  tgjustr  26176  wlkcompim  27329  wwlksnredwwlkn  27589  wwlksnextsurj  27594  upgr4cycl4dv4e  27880  ex-natded5.2-2  28100  chscllem2  29331  chscllem4  29333  nmopge0  29604  nmfnge0  29620  nmoptrii  29787  staddi  29939  stadd3i  29941  atcvatlem  30078  supssd  30360  infssd  30361  xrofsup  30407  xrge0addgt0  30594  archiabllem2c  30740  orngmul  30792  linds2eq  30857  lbsdiflsp0  30910  fedgmullem2  30914  esumpmono  31226  unelldsys  31305  omssubaddlem  31445  signstfvneq0  31730  axtgupdim2ALTV  31827  bnj1098  31943  bnj1110  32140  bnj1121  32143  0nn0m1nnn0  32237  cplgredgex  32253  erdszelem8  32331  txsconn  32374  cvmlift2lem10  32445  cvmlift3lem7  32458  dvdspw  32868  sotrd  32887  dfon2lem6  32919  dfon2lem8  32921  frpomin  32964  nosupbnd1  33100  nosupbnd2lem1  33101  nosupbnd2  33102  noetalem3  33105  slttrd  33124  sltletrd  33125  slelttrd  33126  sletrd  33127  cgrtr4d  33332  cgrtrand  33340  cgrtr3and  33342  cgrextendand  33356  btwnexch3and  33368  btwnexchand  33373  linecgrand  33429  endofsegidand  33433  btwnconn1lem4  33437  btwnconn1lem8  33441  btwnconn1lem11  33444  btwnconn1lem12  33445  brsegle2  33456  seglecgr12im  33457  segleantisym  33462  colinbtwnle  33465  broutsideof2  33469  outsideoftr  33476  outsidele  33479  lineelsb2  33495  linethru  33500  gtinf  33553  copsex2d  34312  relowlssretop  34515  pibt2  34569  heicant  34796  mbfresfi  34807  ftc1anclem6  34841  eqvreltrd  35712  riotasv2d  35962  lcvnbtwn2  36032  lcvnbtwn3  36033  lcvexchlem4  36042  omlfh1N  36263  atlen0  36315  atlatmstc  36324  cvratlem  36426  lnnat  36432  2atlt  36444  athgt  36461  1cvratex  36478  ps-2  36483  llncmp  36527  llncvrlpln  36563  lplncmp  36567  lplncvrlvol  36621  lvolcmp  36622  dalemcea  36665  dalem-cly  36676  dalem10  36678  dalem17  36685  dalem25  36703  dalem38  36715  dalem44  36721  dalem55  36732  2atm2atN  36790  cdlema1N  36796  paddasslem5  36829  dalawlem3  36878  dalawlem7  36882  dalawlem11  36886  dalawlem12  36887  lhp0lt  37008  4atexlemc  37074  cdlemg33a  37711  cdlemg33  37716  cdlemk51  37958  dia2dimlem2  38070  dia2dimlem3  38071  dihmeetlem20N  38331  ismrcd2  39163  pellqrex  39343  jm2.17b  39425  dvdsacongtr  39448  jm2.26lem3  39465  jm2.27a  39469  jm2.27c  39471  fnwe2lem2  39518  addrcom  40674  infxrunb2  41503  0ellimcdiv  41797  stoweidlem15  42168  stoweidlem26  42179  stoweidlem28  42181  stoweidlem32  42185  stoweidlem44  42197  meadjuni  42607  dfatcolem  43322  icceuelpart  43430  perfectALTVlem1  43720  bgoldbtbndlem2  43805  bgoldbtbndlem3  43806  copisnmnd  43910  assintopass  43955  lcoss  44325  islindeps2  44372  isldepslvec2  44374  difmodm1lt  44416
  Copyright terms: Public domain W3C validator