Theorem mp2and 709

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

Step	Hyp	Ref	Expression
1		mp2and.2	. 2 ⊢ (𝜑 → 𝜒)
2		mp2and.1	. . 3 ⊢ (𝜑 → 𝜓)
3		mp2and.3	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
4	2, 3	mpand 705	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
5	1, 4	mpd 15	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  reu2eqd  3700  ssnelpssd  4070  sotrd  5582  frpomin  6327  fvf1pr  7291  tfisi  7839  tfindsg2  7842  mposn  8082  frxp2  8124  smoord  8336  oelimcl  8570  oeeui  8572  nnawordex  8607  omabs  8621  naddssim  8656  naddel12  8671  ertrd  8695  en2prd  9028  omxpenlem  9050  fodomfir  9271  ixpfi2  9291  supssd  9407  infssd  9438  oismo  9486  cantnflem1c  9640  cantnflem1  9642  cantnflem3  9644  infxpenc2  9990  isfin2-2  10287  axdc2lem  10416  r1limwun  10705  letrd  11351  lelttrd  11352  ltletrd  11354  lttrd  11355  le2subd  11818  ltleaddd  11819  leltaddd  11820  lt2subd  11822  ltmul12a  12058  lemul12ad  12144  lemul12bd  12145  lt2halvesd  12479  uzind  12675  uztrn  12867  xrlttrd  13171  xrlelttrd  13172  xrltletrd  13173  xrletrd  13174  supxrunb1  13332  supxrunb2  13333  ixxun  13375  ixxss1  13377  ixxss2  13378  ixxss12  13379  fldiv4p1lem1div2  13855  fldiv4lem1div2uz2  13856  seqf1o  14066  faclbnd3  14315  relexpindlem  15086  01sqrexlem1  15279  01sqrexlem4  15282  01sqrexlem7  15285  abs3lemd  15501  rlimcn3  15627  o1of2  15650  lo1add  15664  lo1mul  15665  modfsummod  15832  mertenslem1  15924  sin01gt0  16232  cos01gt0  16233  sin02gt0  16234  dvds2addd  16336  dvds2subd  16337  dvdstrd  16339  bezoutlem4  16586  mulgcd  16592  lcmgcdeq  16656  mulgcddvds  16699  rpmulgcd2  16700  rpdvds  16704  divgcdcoprmex  16710  phimullem  16824  eulerthlem1  16826  eulerthlem2  16827  prmdiveq  16831  pythagtriplem4  16865  pcqmul  16899  pcgcd1  16923  pcadd  16935  pockthlem  16951  prmreclem2  16963  4sqlem16  17006  ramub1lem1  17072  ramub1lem2  17073  prmgaplem7  17103  iscatd2  17723  cicsym  17847  initoeu2  18059  joinval  18417  meetval  18431  lattrd  18488  latledi  18519  mulgass  19163  gaorber  19358  psgnunilem4  19547  efgredlem  19797  odadd2  19899  dmdprdpr  20101  ablfacrp2  20119  ablfac1b  20122  ablfac1eu  20125  pgpfac1  20132  orngmul  20921  gsumbagdiaglem  21990  mdetunilem1  22679  mdetunilem4  22682  mdetunilem9  22687  neiptoptop  23198  lmcnp  23371  txcls  23671  txlly  23703  txnlly  23704  tx1stc  23717  alexsubALTlem1  24114  prdsmet  24437  blin2  24496  blcvx  24865  tgqioo  24867  metnrmlem3  24929  iscmet3lem2  25361  ovolmge0  25546  ovolunlem2  25567  mbfi1flimlem  25791  mbfmullem  25794  itg2add  25828  dvferm1lem  26053  dvferm2lem  26055  dvlip2  26064  dvge0  26075  dvcvx  26089  dvfsumabs  26092  ftc1a  26106  plyadd  26284  plymul  26285  dgrlb  26303  plydivlem4  26367  vieta1lem2  26382  ulmdvlem3  26472  sinq12gt0  26579  logdivlti  26692  fsumharmonic  27083  mpodvdsmulf1o  27265  dvdsmulf1o  27267  logfacubnd  27292  perfectlem1  27300  dchrptlem2  27336  2sqlem5  27493  2sqlem8  27497  2sqmod  27507  dchrisum0flblem2  27580  pntibndlem2  27662  pntlemr  27673  pntlemp  27681  nosupbnd1  27785  nosupbnd2lem1  27786  nosupbnd2  27787  noinfbnd1  27800  noinfbnd2lem1  27801  noinfbnd2  27802  noetasuplem4  27807  noetainflem4  27811  ltstrd  27834  ltlestrd  27835  leltstrd  27836  lestrd  27837  oldbdayim  27989  mulsproplem5  28220  mulsproplem6  28221  mulsproplem7  28222  mulsproplem8  28223  ltmulsd  28237  bdayfinbndlem1  28567  bdayfinbnd  28569  axtgpasch  28643  tgjustr  28650  wlkcompim  29839  wwlksnredwwlkn  30102  wwlksnextsurj  30107  upgr4cycl4dv4e  30394  ex-natded5.2-2  30614  chscllem2  31848  chscllem4  31850  nmopge0  32121  nmfnge0  32137  nmoptrii  32304  staddi  32456  stadd3i  32458  atcvatlem  32595  xrofsup  32975  xrge0addgt0  33201  archiabllem2c  33381  linds2eq  33570  ssdifidlprm  33648  lbsdiflsp0  33925  fedgmullem2  33929  esumpmono  34378  unelldsys  34457  omssubaddlem  34598  signstfvneq0  34868  axtgupdim2ALTV  34964  bnj1098  35081  bnj1110  35279  bnj1121  35282  0nn0m1nnn0  35467  cplgredgex  35476  erdszelem8  35553  txsconn  35596  cvmlift2lem10  35667  cvmlift3lem7  35680  dfon2lem6  36141  dfon2lem8  36143  cgrtr4d  36340  cgrtrand  36348  cgrtr3and  36350  cgrextendand  36364  btwnexch3and  36376  btwnexchand  36381  linecgrand  36437  endofsegidand  36441  btwnconn1lem4  36445  btwnconn1lem8  36449  btwnconn1lem11  36452  btwnconn1lem12  36453  brsegle2  36464  seglecgr12im  36465  segleantisym  36470  colinbtwnle  36473  broutsideof2  36477  outsideoftr  36484  outsidele  36487  lineelsb2  36503  linethru  36508  gtinf  36684  weiunpo  36830  copsex2d  37636  relowlssretop  37862  pibt2  37916  heicant  38159  mbfresfi  38170  ftc1anclem6  38202  eqvreltrd  39196  riotasv2d  39586  lcvnbtwn2  39656  lcvnbtwn3  39657  lcvexchlem4  39666  omlfh1N  39887  atlen0  39939  atlatmstc  39948  cvratlem  40050  lnnat  40056  2atlt  40068  athgt  40085  1cvratex  40102  ps-2  40107  llncmp  40151  llncvrlpln  40187  lplncmp  40191  lplncvrlvol  40245  lvolcmp  40246  dalemcea  40289  dalem-cly  40300  dalem10  40302  dalem17  40309  dalem25  40327  dalem38  40339  dalem44  40345  dalem55  40356  2atm2atN  40414  cdlema1N  40420  paddasslem5  40453  dalawlem3  40502  dalawlem7  40506  dalawlem11  40510  dalawlem12  40511  lhp0lt  40632  4atexlemc  40698  cdlemg33a  41335  cdlemg33  41340  cdlemk51  41582  dia2dimlem2  41694  dia2dimlem3  41695  dihmeetlem20N  41955  coprmdvds2d  42623  flt4lem2  43234  flt4lem5f  43244  ismrcd2  43285  pellqrex  43461  jm2.17b  43543  jm2.26lem3  43583  fnwe2lem2  43633  omabs2  43914  addrcom  45041  infxrunb2  45934  0ellimcdiv  46214  dvnprodlem1  46511  stoweidlem15  46580  stoweidlem26  46591  stoweidlem28  46593  stoweidlem32  46597  stoweidlem44  46609  meadjuni  47022  natglobalincr  47444  dfatcolem  47840  icceuelpart  48033  perfectALTVlem1  48334  bgoldbtbndlem2  48419  bgoldbtbndlem3  48420  copisnmnd  48782  assintopass  48827  lcoss  49049  islindeps2  49096  isldepslvec2  49098  isisod  49639  euendfunc  50138