Theorem mp2and 701

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 697	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
5	1, 4	mpd 15	1 ⊢ (𝜑 → 𝜃)

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  3680  ssnelpssd  4049  sotrd  5555  frpomin  6294  fvf1pr  7254  tfisi  7802  tfindsg2  7805  mposn  8045  frxp2  8087  smoord  8298  oelimcl  8529  oeeui  8531  nnawordex  8566  omabs  8580  naddssim  8614  naddel12  8629  ertrd  8653  en2prd  8987  omxpenlem  9009  fodomfir  9231  ixpfi2  9253  supssd  9369  infssd  9400  oismo  9448  cantnflem1c  9602  cantnflem1  9604  cantnflem3  9606  infxpenc2  9938  isfin2-2  10235  axdc2lem  10364  r1limwun  10653  letrd  11297  lelttrd  11298  ltletrd  11300  lttrd  11301  le2subd  11764  ltleaddd  11765  leltaddd  11766  lt2subd  11768  ltmul12a  12005  lemul12ad  12092  lemul12bd  12093  lt2halvesd  12419  uzind  12615  uztrn  12800  xrlttrd  13104  xrlelttrd  13105  xrltletrd  13106  xrletrd  13107  supxrunb1  13265  supxrunb2  13266  ixxun  13308  ixxss1  13310  ixxss2  13311  ixxss12  13312  fldiv4p1lem1div2  13788  fldiv4lem1div2uz2  13789  seqf1o  13999  faclbnd3  14248  relexpindlem  15019  01sqrexlem1  15198  01sqrexlem4  15201  01sqrexlem7  15204  abs3lemd  15420  rlimcn3  15546  o1of2  15569  lo1add  15583  lo1mul  15584  modfsummod  15751  mertenslem1  15843  sin01gt0  16151  cos01gt0  16152  sin02gt0  16153  dvds2addd  16255  dvds2subd  16256  dvdstrd  16258  bezoutlem4  16505  mulgcd  16511  lcmgcdeq  16575  mulgcddvds  16618  rpmulgcd2  16619  rpdvds  16623  divgcdcoprmex  16629  phimullem  16743  eulerthlem1  16745  eulerthlem2  16746  prmdiveq  16750  pythagtriplem4  16784  pcqmul  16818  pcgcd1  16842  pcadd  16854  pockthlem  16870  prmreclem2  16882  4sqlem16  16925  ramub1lem1  16991  ramub1lem2  16992  prmgaplem7  17022  iscatd2  17641  cicsym  17765  initoeu2  17977  joinval  18335  meetval  18349  lattrd  18406  latledi  18437  mulgass  19081  gaorber  19277  psgnunilem4  19466  efgredlem  19716  odadd2  19818  dmdprdpr  20020  ablfacrp2  20038  ablfac1b  20041  ablfac1eu  20044  pgpfac1  20051  orngmul  20840  gsumbagdiaglem  21909  mdetunilem1  22598  mdetunilem4  22601  mdetunilem9  22606  neiptoptop  23117  lmcnp  23290  txcls  23590  txlly  23622  txnlly  23623  tx1stc  23636  alexsubALTlem1  24033  prdsmet  24356  blin2  24415  blcvx  24784  tgqioo  24786  metnrmlem3  24848  iscmet3lem2  25280  ovolmge0  25465  ovolunlem2  25486  mbfi1flimlem  25710  mbfmullem  25713  itg2add  25747  dvferm1lem  25972  dvferm2lem  25974  dvlip2  25983  dvge0  25994  dvcvx  26008  dvfsumabs  26011  ftc1a  26025  plyadd  26203  plymul  26204  dgrlb  26222  plydivlem4  26283  vieta1lem2  26298  ulmdvlem3  26388  sinq12gt0  26492  logdivlti  26605  fsumharmonic  26996  mpodvdsmulf1o  27178  dvdsmulf1o  27180  logfacubnd  27205  perfectlem1  27213  dchrptlem2  27249  2sqlem5  27406  2sqlem8  27410  2sqmod  27420  dchrisum0flblem2  27493  pntibndlem2  27575  pntlemr  27586  pntlemp  27594  nosupbnd1  27699  nosupbnd2lem1  27700  nosupbnd2  27701  noinfbnd1  27714  noinfbnd2lem1  27715  noinfbnd2  27716  noetasuplem4  27721  noetainflem4  27725  ltstrd  27748  ltlestrd  27749  leltstrd  27750  lestrd  27751  oldbdayim  27902  mulsproplem5  28133  mulsproplem6  28134  mulsproplem7  28135  mulsproplem8  28136  ltmulsd  28150  bdayfinbndlem1  28480  bdayfinbnd  28482  axtgpasch  28556  tgjustr  28563  wlkcompim  29721  wwlksnredwwlkn  29984  wwlksnextsurj  29989  upgr4cycl4dv4e  30276  ex-natded5.2-2  30496  chscllem2  31730  chscllem4  31732  nmopge0  32003  nmfnge0  32019  nmoptrii  32186  staddi  32338  stadd3i  32340  atcvatlem  32477  xrofsup  32862  xrge0addgt0  33099  archiabllem2c  33279  linds2eq  33467  ssdifidlprm  33544  lbsdiflsp0  33813  fedgmullem2  33817  esumpmono  34266  unelldsys  34345  omssubaddlem  34486  signstfvneq0  34759  axtgupdim2ALTV  34855  bnj1098  34969  bnj1110  35167  bnj1121  35170  0nn0m1nnn0  35338  cplgredgex  35346  erdszelem8  35423  txsconn  35466  cvmlift2lem10  35537  cvmlift3lem7  35550  dfon2lem6  36011  dfon2lem8  36013  cgrtr4d  36210  cgrtrand  36218  cgrtr3and  36220  cgrextendand  36234  btwnexch3and  36246  btwnexchand  36251  linecgrand  36307  endofsegidand  36311  btwnconn1lem4  36315  btwnconn1lem8  36319  btwnconn1lem11  36322  btwnconn1lem12  36323  brsegle2  36334  seglecgr12im  36335  segleantisym  36340  colinbtwnle  36343  broutsideof2  36347  outsideoftr  36354  outsidele  36357  lineelsb2  36373  linethru  36378  gtinf  36544  weiunpo  36690  copsex2d  37496  relowlssretop  37722  pibt2  37776  heicant  38019  mbfresfi  38030  ftc1anclem6  38062  eqvreltrd  39056  riotasv2d  39446  lcvnbtwn2  39516  lcvnbtwn3  39517  lcvexchlem4  39526  omlfh1N  39747  atlen0  39799  atlatmstc  39808  cvratlem  39910  lnnat  39916  2atlt  39928  athgt  39945  1cvratex  39962  ps-2  39967  llncmp  40011  llncvrlpln  40047  lplncmp  40051  lplncvrlvol  40105  lvolcmp  40106  dalemcea  40149  dalem-cly  40160  dalem10  40162  dalem17  40169  dalem25  40187  dalem38  40199  dalem44  40205  dalem55  40216  2atm2atN  40274  cdlema1N  40280  paddasslem5  40313  dalawlem3  40362  dalawlem7  40366  dalawlem11  40370  dalawlem12  40371  lhp0lt  40492  4atexlemc  40558  cdlemg33a  41195  cdlemg33  41200  cdlemk51  41442  dia2dimlem2  41554  dia2dimlem3  41555  dihmeetlem20N  41815  coprmdvds2d  42483  flt4lem2  43094  flt4lem5f  43104  ismrcd2  43145  pellqrex  43321  jm2.17b  43403  jm2.26lem3  43443  fnwe2lem2  43493  omabs2  43774  addrcom  44915  infxrunb2  45809  0ellimcdiv  46089  dvnprodlem1  46386  stoweidlem15  46455  stoweidlem26  46466  stoweidlem28  46468  stoweidlem32  46472  stoweidlem44  46484  meadjuni  46897  natglobalincr  47319  dfatcolem  47715  icceuelpart  47908  perfectALTVlem1  48209  bgoldbtbndlem2  48294  bgoldbtbndlem3  48295  copisnmnd  48657  assintopass  48702  lcoss  48924  islindeps2  48971  isldepslvec2  48973  isisod  49514  euendfunc  50013