Theorem mp2and 711

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  reu2eqd  3698  ssnelpssd  4069  sotrd  5595  frpomin  6341  fvf1pr  7305  tfisi  7854  tfindsg2  7857  mposn  8097  frxp2  8139  smoord  8351  oelimcl  8585  oeeui  8587  nnawordex  8622  omabs  8636  naddssim  8671  naddel12  8686  ertrd  8710  en2prd  9043  omxpenlem  9065  fodomfir  9286  ixpfi2  9306  supssd  9422  infssd  9453  oismo  9501  cantnflem1c  9655  cantnflem1  9657  cantnflem3  9659  infxpenc2  10005  isfin2-2  10302  axdc2lem  10431  r1limwun  10720  letrd  11366  lelttrd  11367  ltletrd  11369  lttrd  11370  le2subd  11833  ltleaddd  11834  leltaddd  11835  lt2subd  11837  ltmul12a  12070  lemul12ad  12156  lemul12bd  12157  lt2halvesd  12491  uzind  12687  uztrn  12879  xrlttrd  13183  xrlelttrd  13184  xrltletrd  13185  xrletrd  13186  supxrunb1  13344  supxrunb2  13345  ixxun  13387  ixxss1  13389  ixxss2  13390  ixxss12  13391  fldiv4p1lem1div2  13867  fldiv4lem1div2uz2  13868  seqf1o  14078  faclbnd3  14327  relexpindlem  15099  01sqrexlem1  15292  01sqrexlem4  15295  01sqrexlem7  15298  abs3lemd  15514  rlimcn3  15640  o1of2  15663  lo1add  15677  lo1mul  15678  modfsummod  15845  mertenslem1  15937  sin01gt0  16245  cos01gt0  16246  sin02gt0  16247  dvds2addd  16349  dvds2subd  16350  dvdstrd  16352  bezoutlem4  16599  mulgcd  16605  lcmgcdeq  16669  mulgcddvds  16712  rpmulgcd2  16713  rpdvds  16717  divgcdcoprmex  16723  phimullem  16837  eulerthlem1  16839  eulerthlem2  16840  prmdiveq  16844  pythagtriplem4  16878  pcqmul  16912  pcgcd1  16936  pcadd  16948  pockthlem  16964  prmreclem2  16976  4sqlem16  17019  ramub1lem1  17085  ramub1lem2  17086  prmgaplem7  17116  iscatd2  17736  cicsym  17860  initoeu2  18072  joinval  18430  meetval  18444  lattrd  18501  latledi  18532  mulgass  19176  gaorber  19377  psgnunilem4  19566  efgredlem  19816  odadd2  19918  dmdprdpr  20120  ablfacrp2  20138  ablfac1b  20141  ablfac1eu  20144  pgpfac1  20151  orngmul  20947  ssdifidlprm  21465  gsumbagdiaglem  22060  mdetunilem1  22748  mdetunilem4  22751  mdetunilem9  22756  neiptoptop  23267  lmcnp  23440  txcls  23740  txlly  23772  txnlly  23773  tx1stc  23786  alexsubALTlem1  24183  prdsmet  24506  blin2  24565  blcvx  24934  tgqioo  24936  metnrmlem3  24998  iscmet3lem2  25430  ovolmge0  25615  ovolunlem2  25636  mbfi1flimlem  25860  mbfmullem  25863  itg2add  25897  dvferm1lem  26122  dvferm2lem  26124  dvlip2  26133  dvge0  26144  dvcvx  26158  dvfsumabs  26161  ftc1a  26175  plyadd  26353  plymul  26354  dgrlb  26372  plydivlem4  26436  vieta1lem2  26451  ulmdvlem3  26541  sinq12gt0  26648  logdivlti  26761  fsumharmonic  27152  mpodvdsmulf1o  27334  dvdsmulf1o  27336  logfacubnd  27361  perfectlem1  27369  dchrptlem2  27405  2sqlem5  27562  2sqlem8  27566  2sqmod  27576  dchrisum0flblem2  27649  pntibndlem2  27731  pntlemr  27742  pntlemp  27750  nosupbnd1  27854  nosupbnd2lem1  27855  nosupbnd2  27856  noinfbnd1  27869  noinfbnd2lem1  27870  noinfbnd2  27871  noetasuplem4  27876  noetainflem4  27880  ltstrd  27903  ltlestrd  27904  leltstrd  27905  lestrd  27906  oldbdayim  28058  mulsproplem5  28289  mulsproplem6  28290  mulsproplem7  28291  mulsproplem8  28292  ltmulsd  28306  bdayfinbndlem1  28636  bdayfinbnd  28638  axtgpasch  28712  tgjustr  28719  wlkcompim  29947  wwlksnredwwlkn  30210  wwlksnextsurj  30215  upgr4cycl4dv4e  30502  ex-natded5.2-2  30722  chscllem2  31956  chscllem4  31958  nmopge0  32229  nmfnge0  32245  nmoptrii  32412  staddi  32564  stadd3i  32566  atcvatlem  32703  xrofsup  33078  xrge0addgt0  33303  archiabllem2c  33481  linds2eq  33660  lbsdiflsp0  33982  fedgmullem2  33986  esumpmono  34435  unelldsys  34514  omssubaddlem  34655  signstfvneq0  34925  axtgupdim2ALTV  35021  bnj1098  35138  bnj1110  35336  bnj1121  35339  0nn0m1nnn0  35558  cplgredgex  35567  erdszelem8  35644  txsconn  35687  cvmlift2lem10  35758  cvmlift3lem7  35771  dfon2lem6  36232  dfon2lem8  36234  cgrtr4d  36431  cgrtrand  36439  cgrtr3and  36441  cgrextendand  36455  btwnexch3and  36467  btwnexchand  36472  linecgrand  36528  endofsegidand  36532  btwnconn1lem4  36536  btwnconn1lem8  36540  btwnconn1lem11  36543  btwnconn1lem12  36544  brsegle2  36555  seglecgr12im  36556  segleantisym  36561  colinbtwnle  36564  broutsideof2  36568  outsideoftr  36575  outsidele  36578  lineelsb2  36594  linethru  36599  gtinf  36774  weiunpo  36920  copsex2d  37727  relowlssretop  37953  pibt2  38007  heicant  38250  mbfresfi  38261  ftc1anclem6  38293  eqvreltrd  39287  riotasv2d  39677  lcvnbtwn2  39747  lcvnbtwn3  39748  lcvexchlem4  39757  omlfh1N  39978  atlen0  40030  atlatmstc  40039  cvratlem  40141  lnnat  40147  2atlt  40159  athgt  40176  1cvratex  40193  ps-2  40198  llncmp  40242  llncvrlpln  40278  lplncmp  40282  lplncvrlvol  40336  lvolcmp  40337  dalemcea  40380  dalem-cly  40391  dalem10  40393  dalem17  40400  dalem25  40418  dalem38  40430  dalem44  40436  dalem55  40447  2atm2atN  40505  cdlema1N  40511  paddasslem5  40544  dalawlem3  40593  dalawlem7  40597  dalawlem11  40601  dalawlem12  40602  lhp0lt  40723  4atexlemc  40789  cdlemg33a  41426  cdlemg33  41431  cdlemk51  41673  dia2dimlem2  41785  dia2dimlem3  41786  dihmeetlem20N  42046  coprmdvds2d  42714  flt4lem2  43327  flt4lem5f  43337  ismrcd2  43378  pellqrex  43554  jm2.17b  43636  jm2.26lem3  43676  fnwe2lem2  43726  omabs2  44007  addrcom  45131  infxrunb2  46031  0ellimcdiv  46311  dvnprodlem1  46608  stoweidlem15  46677  stoweidlem26  46688  stoweidlem28  46690  stoweidlem32  46694  stoweidlem44  46706  meadjuni  47119  natglobalincr  47541  dfatcolem  47937  icceuelpart  48130  perfectALTVlem1  48431  bgoldbtbndlem2  48516  bgoldbtbndlem3  48517  copisnmnd  48879  assintopass  48924  lcoss  49161  islindeps2  49208  isldepslvec2  49210  isisod  49750  euendfunc  50249