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  3693  ssnelpssd  4063  sotrd  5548  frpomin  6283  fvf1pr  7236  tfisi  7784  tfindsg2  7787  mposn  8028  frxp2  8069  smoord  8280  oelimcl  8510  oeeui  8512  nnawordex  8547  omabs  8561  naddssim  8595  naddel12  8610  ertrd  8633  en2prd  8964  omxpenlem  8986  fodomfir  9207  ixpfi2  9229  supssd  9342  infssd  9373  oismo  9421  cantnflem1c  9572  cantnflem1  9574  cantnflem3  9576  infxpenc2  9905  isfin2-2  10202  axdc2lem  10331  r1limwun  10619  letrd  11262  lelttrd  11263  ltletrd  11265  lttrd  11266  le2subd  11729  ltleaddd  11730  leltaddd  11731  lt2subd  11733  ltmul12a  11969  lemul12ad  12056  lemul12bd  12057  lt2halvesd  12361  uzind  12557  uztrn  12742  xrlttrd  13050  xrlelttrd  13051  xrltletrd  13052  xrletrd  13053  supxrunb1  13210  supxrunb2  13211  ixxun  13253  ixxss1  13255  ixxss2  13256  ixxss12  13257  fldiv4p1lem1div2  13731  fldiv4lem1div2uz2  13732  seqf1o  13942  faclbnd3  14191  relexpindlem  14962  01sqrexlem1  15141  01sqrexlem4  15144  01sqrexlem7  15147  abs3lemd  15363  rlimcn3  15489  o1of2  15512  lo1add  15526  lo1mul  15527  modfsummod  15693  mertenslem1  15783  sin01gt0  16091  cos01gt0  16092  sin02gt0  16093  dvds2addd  16195  dvds2subd  16196  dvdstrd  16198  bezoutlem4  16445  mulgcd  16451  lcmgcdeq  16515  mulgcddvds  16558  rpmulgcd2  16559  rpdvds  16563  divgcdcoprmex  16569  phimullem  16682  eulerthlem1  16684  eulerthlem2  16685  prmdiveq  16689  pythagtriplem4  16723  pcqmul  16757  pcgcd1  16781  pcadd  16793  pockthlem  16809  prmreclem2  16821  4sqlem16  16864  ramub1lem1  16930  ramub1lem2  16931  prmgaplem7  16961  iscatd2  17579  cicsym  17703  initoeu2  17915  joinval  18273  meetval  18287  lattrd  18344  latledi  18375  mulgass  19016  gaorber  19213  psgnunilem4  19402  efgredlem  19652  odadd2  19754  dmdprdpr  19956  ablfacrp2  19974  ablfac1b  19977  ablfac1eu  19980  pgpfac1  19987  orngmul  20773  gsumbagdiaglem  21860  mdetunilem1  22520  mdetunilem4  22523  mdetunilem9  22528  neiptoptop  23039  lmcnp  23212  txcls  23512  txlly  23544  txnlly  23545  tx1stc  23558  alexsubALTlem1  23955  prdsmet  24278  blin2  24337  blcvx  24706  tgqioo  24708  metnrmlem3  24770  iscmet3lem2  25212  ovolmge0  25398  ovolunlem2  25419  mbfi1flimlem  25643  mbfmullem  25646  itg2add  25680  dvferm1lem  25908  dvferm2lem  25910  dvlip2  25920  dvge0  25931  dvcvx  25945  dvfsumabs  25949  ftc1a  25964  plyadd  26142  plymul  26143  dgrlb  26161  plydivlem4  26224  vieta1lem2  26239  ulmdvlem3  26331  sinq12gt0  26436  logdivlti  26549  fsumharmonic  26942  mpodvdsmulf1o  27124  dvdsmulf1o  27126  logfacubnd  27152  perfectlem1  27160  dchrptlem2  27196  2sqlem5  27353  2sqlem8  27357  2sqmod  27367  dchrisum0flblem2  27440  pntibndlem2  27522  pntlemr  27533  pntlemp  27541  nosupbnd1  27646  nosupbnd2lem1  27647  nosupbnd2  27648  noinfbnd1  27661  noinfbnd2lem1  27662  noinfbnd2  27663  noetasuplem4  27668  noetainflem4  27672  slttrd  27691  sltletrd  27692  slelttrd  27693  sletrd  27694  oldbdayim  27827  mulsproplem5  28052  mulsproplem6  28053  mulsproplem7  28054  mulsproplem8  28055  sltmuld  28069  axtgpasch  28438  tgjustr  28445  wlkcompim  29603  wwlksnredwwlkn  29866  wwlksnextsurj  29871  upgr4cycl4dv4e  30155  ex-natded5.2-2  30375  chscllem2  31608  chscllem4  31610  nmopge0  31881  nmfnge0  31897  nmoptrii  32064  staddi  32216  stadd3i  32218  atcvatlem  32355  xrofsup  32740  xrge0addgt0  32988  archiabllem2c  33154  linds2eq  33336  ssdifidlprm  33413  lbsdiflsp0  33629  fedgmullem2  33633  esumpmono  34082  unelldsys  34161  omssubaddlem  34302  signstfvneq0  34575  axtgupdim2ALTV  34671  bnj1098  34785  bnj1110  34984  bnj1121  34987  0nn0m1nnn0  35125  cplgredgex  35133  erdszelem8  35210  txsconn  35253  cvmlift2lem10  35324  cvmlift3lem7  35337  dfon2lem6  35801  dfon2lem8  35803  cgrtr4d  35998  cgrtrand  36006  cgrtr3and  36008  cgrextendand  36022  btwnexch3and  36034  btwnexchand  36039  linecgrand  36095  endofsegidand  36099  btwnconn1lem4  36103  btwnconn1lem8  36107  btwnconn1lem11  36110  btwnconn1lem12  36111  brsegle2  36122  seglecgr12im  36123  segleantisym  36128  colinbtwnle  36131  broutsideof2  36135  outsideoftr  36142  outsidele  36145  lineelsb2  36161  linethru  36166  gtinf  36332  weiunpo  36478  copsex2d  37152  relowlssretop  37376  pibt2  37430  heicant  37674  mbfresfi  37685  ftc1anclem6  37717  eqvreltrd  38624  riotasv2d  38975  lcvnbtwn2  39045  lcvnbtwn3  39046  lcvexchlem4  39055  omlfh1N  39276  atlen0  39328  atlatmstc  39337  cvratlem  39439  lnnat  39445  2atlt  39457  athgt  39474  1cvratex  39491  ps-2  39496  llncmp  39540  llncvrlpln  39576  lplncmp  39580  lplncvrlvol  39634  lvolcmp  39635  dalemcea  39678  dalem-cly  39689  dalem10  39691  dalem17  39698  dalem25  39716  dalem38  39728  dalem44  39734  dalem55  39745  2atm2atN  39803  cdlema1N  39809  paddasslem5  39842  dalawlem3  39891  dalawlem7  39895  dalawlem11  39899  dalawlem12  39900  lhp0lt  40021  4atexlemc  40087  cdlemg33a  40724  cdlemg33  40729  cdlemk51  40971  dia2dimlem2  41083  dia2dimlem3  41084  dihmeetlem20N  41344  coprmdvds2d  42013  flt4lem2  42659  flt4lem5f  42669  ismrcd2  42711  pellqrex  42891  jm2.17b  42973  jm2.26lem3  43013  fnwe2lem2  43063  omabs2  43344  addrcom  44486  infxrunb2  45385  0ellimcdiv  45666  dvnprodlem1  45963  stoweidlem15  46032  stoweidlem26  46043  stoweidlem28  46045  stoweidlem32  46049  stoweidlem44  46061  meadjuni  46474  natglobalincr  46894  dfatcolem  47265  icceuelpart  47446  perfectALTVlem1  47731  bgoldbtbndlem2  47816  bgoldbtbndlem3  47817  copisnmnd  48179  assintopass  48224  lcoss  48447  islindeps2  48494  isldepslvec2  48496  isisod  49038  euendfunc  49537