Theorem mp2and 699

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  reu2eqd  3742  ssnelpssd  4115  sotrd  5618  frpomin  6361  fvf1pr  7327  tfisi  7880  tfindsg2  7883  mposn  8128  frxp2  8169  smoord  8405  oelimcl  8638  oeeui  8640  nnawordex  8675  omabs  8689  naddssim  8723  naddel12  8738  ertrd  8761  en2prd  9088  omxpenlem  9113  fodomfir  9368  ixpfi2  9390  oismo  9580  cantnflem1c  9727  cantnflem1  9729  cantnflem3  9731  infxpenc2  10062  isfin2-2  10359  axdc2lem  10488  r1limwun  10776  letrd  11418  lelttrd  11419  ltletrd  11421  lttrd  11422  le2addd  11882  le2subd  11883  ltleaddd  11884  leltaddd  11885  lt2subd  11887  ltmul12a  12123  lemul12ad  12210  lemul12bd  12211  lt2halvesd  12514  uzind  12710  uztrn  12896  xrlttrd  13201  xrlelttrd  13202  xrltletrd  13203  xrletrd  13204  supxrunb1  13361  supxrunb2  13362  ixxun  13403  ixxss1  13405  ixxss2  13406  ixxss12  13407  fldiv4p1lem1div2  13875  fldiv4lem1div2uz2  13876  seqf1o  14084  faclbnd3  14331  relexpindlem  15102  01sqrexlem1  15281  01sqrexlem4  15284  01sqrexlem7  15287  abs3lemd  15500  rlimcn3  15626  o1of2  15649  lo1add  15663  lo1mul  15664  modfsummod  15830  mertenslem1  15920  sin01gt0  16226  cos01gt0  16227  sin02gt0  16228  dvds2addd  16329  dvds2subd  16330  dvdstrd  16332  bezoutlem4  16579  mulgcd  16585  lcmgcdeq  16649  mulgcddvds  16692  rpmulgcd2  16693  rpdvds  16697  divgcdcoprmex  16703  phimullem  16816  eulerthlem1  16818  eulerthlem2  16819  prmdiveq  16823  pythagtriplem4  16857  pcqmul  16891  pcgcd1  16915  pcadd  16927  pockthlem  16943  prmreclem2  16955  4sqlem16  16998  ramub1lem1  17064  ramub1lem2  17065  prmgaplem7  17095  iscatd2  17724  cicsym  17848  initoeu2  18061  joinval  18422  meetval  18436  lattrd  18491  latledi  18522  mulgass  19129  gaorber  19326  psgnunilem4  19515  efgredlem  19765  odadd2  19867  dmdprdpr  20069  ablfacrp2  20087  ablfac1b  20090  ablfac1eu  20093  pgpfac1  20100  gsumbagdiaglem  21950  mdetunilem1  22618  mdetunilem4  22621  mdetunilem9  22626  neiptoptop  23139  lmcnp  23312  txcls  23612  txlly  23644  txnlly  23645  tx1stc  23658  alexsubALTlem1  24055  prdsmet  24380  blin2  24439  blcvx  24819  tgqioo  24821  metnrmlem3  24883  iscmet3lem2  25326  ovolmge0  25512  ovolunlem2  25533  mbfi1flimlem  25757  mbfmullem  25760  itg2add  25794  dvferm1lem  26022  dvferm2lem  26024  dvlip2  26034  dvge0  26045  dvcvx  26059  dvfsumabs  26063  ftc1a  26078  plyadd  26256  plymul  26257  dgrlb  26275  plydivlem4  26338  vieta1lem2  26353  ulmdvlem3  26445  sinq12gt0  26549  logdivlti  26662  fsumharmonic  27055  mpodvdsmulf1o  27237  dvdsmulf1o  27239  logfacubnd  27265  perfectlem1  27273  dchrptlem2  27309  2sqlem5  27466  2sqlem8  27470  2sqmod  27480  dchrisum0flblem2  27553  pntibndlem2  27635  pntlemr  27646  pntlemp  27654  nosupbnd1  27759  nosupbnd2lem1  27760  nosupbnd2  27761  noinfbnd1  27774  noinfbnd2lem1  27775  noinfbnd2  27776  noetasuplem4  27781  noetainflem4  27785  slttrd  27804  sltletrd  27805  slelttrd  27806  sletrd  27807  oldbdayim  27927  mulsproplem5  28146  mulsproplem6  28147  mulsproplem7  28148  mulsproplem8  28149  sltmuld  28163  axtgpasch  28475  tgjustr  28482  wlkcompim  29650  wwlksnredwwlkn  29915  wwlksnextsurj  29920  upgr4cycl4dv4e  30204  ex-natded5.2-2  30424  chscllem2  31657  chscllem4  31659  nmopge0  31930  nmfnge0  31946  nmoptrii  32113  staddi  32265  stadd3i  32267  atcvatlem  32404  supssd  32721  infssd  32722  xrofsup  32771  xrge0addgt0  33022  archiabllem2c  33202  orngmul  33333  linds2eq  33409  ssdifidlprm  33486  lbsdiflsp0  33677  fedgmullem2  33681  esumpmono  34080  unelldsys  34159  omssubaddlem  34301  signstfvneq0  34587  axtgupdim2ALTV  34683  bnj1098  34797  bnj1110  34996  bnj1121  34999  0nn0m1nnn0  35118  cplgredgex  35126  erdszelem8  35203  txsconn  35246  cvmlift2lem10  35317  cvmlift3lem7  35330  dfon2lem6  35789  dfon2lem8  35791  cgrtr4d  35986  cgrtrand  35994  cgrtr3and  35996  cgrextendand  36010  btwnexch3and  36022  btwnexchand  36027  linecgrand  36083  endofsegidand  36087  btwnconn1lem4  36091  btwnconn1lem8  36095  btwnconn1lem11  36098  btwnconn1lem12  36099  brsegle2  36110  seglecgr12im  36111  segleantisym  36116  colinbtwnle  36119  broutsideof2  36123  outsideoftr  36130  outsidele  36133  lineelsb2  36149  linethru  36154  gtinf  36320  weiunpo  36466  copsex2d  37140  relowlssretop  37364  pibt2  37418  heicant  37662  mbfresfi  37673  ftc1anclem6  37705  eqvreltrd  38609  riotasv2d  38958  lcvnbtwn2  39028  lcvnbtwn3  39029  lcvexchlem4  39038  omlfh1N  39259  atlen0  39311  atlatmstc  39320  cvratlem  39423  lnnat  39429  2atlt  39441  athgt  39458  1cvratex  39475  ps-2  39480  llncmp  39524  llncvrlpln  39560  lplncmp  39564  lplncvrlvol  39618  lvolcmp  39619  dalemcea  39662  dalem-cly  39673  dalem10  39675  dalem17  39682  dalem25  39700  dalem38  39712  dalem44  39718  dalem55  39729  2atm2atN  39787  cdlema1N  39793  paddasslem5  39826  dalawlem3  39875  dalawlem7  39879  dalawlem11  39883  dalawlem12  39884  lhp0lt  40005  4atexlemc  40071  cdlemg33a  40708  cdlemg33  40713  cdlemk51  40955  dia2dimlem2  41067  dia2dimlem3  41068  dihmeetlem20N  41328  coprmdvds2d  42002  flt4lem2  42657  flt4lem5f  42667  ismrcd2  42710  pellqrex  42890  jm2.17b  42973  jm2.26lem3  43013  fnwe2lem2  43063  omabs2  43345  addrcom  44494  infxrunb2  45379  0ellimcdiv  45664  dvnprodlem1  45961  stoweidlem15  46030  stoweidlem26  46041  stoweidlem28  46043  stoweidlem32  46047  stoweidlem44  46059  meadjuni  46472  natglobalincr  46892  dfatcolem  47267  icceuelpart  47423  perfectALTVlem1  47708  bgoldbtbndlem2  47793  bgoldbtbndlem3  47794  copisnmnd  48085  assintopass  48130  lcoss  48353  islindeps2  48400  isldepslvec2  48402  difmodm1lt  48443  isisod  48910