Theorem mp2and 700

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 696	. 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  3683  ssnelpssd  4056  sotrd  5565  frpomin  6305  fvf1pr  7262  tfisi  7810  tfindsg2  7813  mposn  8053  frxp2  8094  smoord  8305  oelimcl  8536  oeeui  8538  nnawordex  8573  omabs  8587  naddssim  8621  naddel12  8636  ertrd  8660  en2prd  8994  omxpenlem  9016  fodomfir  9238  ixpfi2  9260  supssd  9376  infssd  9407  oismo  9455  cantnflem1c  9608  cantnflem1  9610  cantnflem3  9612  infxpenc2  9944  isfin2-2  10241  axdc2lem  10370  r1limwun  10659  letrd  11303  lelttrd  11304  ltletrd  11306  lttrd  11307  le2subd  11770  ltleaddd  11771  leltaddd  11772  lt2subd  11774  ltmul12a  12011  lemul12ad  12098  lemul12bd  12099  lt2halvesd  12425  uzind  12621  uztrn  12806  xrlttrd  13110  xrlelttrd  13111  xrltletrd  13112  xrletrd  13113  supxrunb1  13271  supxrunb2  13272  ixxun  13314  ixxss1  13316  ixxss2  13317  ixxss12  13318  fldiv4p1lem1div2  13794  fldiv4lem1div2uz2  13795  seqf1o  14005  faclbnd3  14254  relexpindlem  15025  01sqrexlem1  15204  01sqrexlem4  15207  01sqrexlem7  15210  abs3lemd  15426  rlimcn3  15552  o1of2  15575  lo1add  15589  lo1mul  15590  modfsummod  15757  mertenslem1  15849  sin01gt0  16157  cos01gt0  16158  sin02gt0  16159  dvds2addd  16261  dvds2subd  16262  dvdstrd  16264  bezoutlem4  16511  mulgcd  16517  lcmgcdeq  16581  mulgcddvds  16624  rpmulgcd2  16625  rpdvds  16629  divgcdcoprmex  16635  phimullem  16749  eulerthlem1  16751  eulerthlem2  16752  prmdiveq  16756  pythagtriplem4  16790  pcqmul  16824  pcgcd1  16848  pcadd  16860  pockthlem  16876  prmreclem2  16888  4sqlem16  16931  ramub1lem1  16997  ramub1lem2  16998  prmgaplem7  17028  iscatd2  17647  cicsym  17771  initoeu2  17983  joinval  18341  meetval  18355  lattrd  18412  latledi  18443  mulgass  19087  gaorber  19283  psgnunilem4  19472  efgredlem  19722  odadd2  19824  dmdprdpr  20026  ablfacrp2  20044  ablfac1b  20047  ablfac1eu  20050  pgpfac1  20057  orngmul  20842  gsumbagdiaglem  21910  mdetunilem1  22577  mdetunilem4  22580  mdetunilem9  22585  neiptoptop  23096  lmcnp  23269  txcls  23569  txlly  23601  txnlly  23602  tx1stc  23615  alexsubALTlem1  24012  prdsmet  24335  blin2  24394  blcvx  24763  tgqioo  24765  metnrmlem3  24827  iscmet3lem2  25259  ovolmge0  25444  ovolunlem2  25465  mbfi1flimlem  25689  mbfmullem  25692  itg2add  25726  dvferm1lem  25951  dvferm2lem  25953  dvlip2  25962  dvge0  25973  dvcvx  25987  dvfsumabs  25990  ftc1a  26004  plyadd  26182  plymul  26183  dgrlb  26201  plydivlem4  26262  vieta1lem2  26277  ulmdvlem3  26367  sinq12gt0  26471  logdivlti  26584  fsumharmonic  26975  mpodvdsmulf1o  27157  dvdsmulf1o  27159  logfacubnd  27184  perfectlem1  27192  dchrptlem2  27228  2sqlem5  27385  2sqlem8  27389  2sqmod  27399  dchrisum0flblem2  27472  pntibndlem2  27554  pntlemr  27565  pntlemp  27573  nosupbnd1  27678  nosupbnd2lem1  27679  nosupbnd2  27680  noinfbnd1  27693  noinfbnd2lem1  27694  noinfbnd2  27695  noetasuplem4  27700  noetainflem4  27704  ltstrd  27727  ltlestrd  27728  leltstrd  27729  lestrd  27730  oldbdayim  27881  mulsproplem5  28112  mulsproplem6  28113  mulsproplem7  28114  mulsproplem8  28115  ltmulsd  28129  bdayfinbndlem1  28459  bdayfinbnd  28461  axtgpasch  28535  tgjustr  28542  wlkcompim  29700  wwlksnredwwlkn  29963  wwlksnextsurj  29968  upgr4cycl4dv4e  30255  ex-natded5.2-2  30475  chscllem2  31709  chscllem4  31711  nmopge0  31982  nmfnge0  31998  nmoptrii  32165  staddi  32317  stadd3i  32319  atcvatlem  32456  xrofsup  32840  xrge0addgt0  33077  archiabllem2c  33256  linds2eq  33441  ssdifidlprm  33518  lbsdiflsp0  33770  fedgmullem2  33774  esumpmono  34223  unelldsys  34302  omssubaddlem  34443  signstfvneq0  34716  axtgupdim2ALTV  34812  bnj1098  34926  bnj1110  35124  bnj1121  35127  0nn0m1nnn0  35295  cplgredgex  35303  erdszelem8  35380  txsconn  35423  cvmlift2lem10  35494  cvmlift3lem7  35507  dfon2lem6  35968  dfon2lem8  35970  cgrtr4d  36167  cgrtrand  36175  cgrtr3and  36177  cgrextendand  36191  btwnexch3and  36203  btwnexchand  36208  linecgrand  36264  endofsegidand  36268  btwnconn1lem4  36272  btwnconn1lem8  36276  btwnconn1lem11  36279  btwnconn1lem12  36280  brsegle2  36291  seglecgr12im  36292  segleantisym  36297  colinbtwnle  36300  broutsideof2  36304  outsideoftr  36311  outsidele  36314  lineelsb2  36330  linethru  36335  gtinf  36501  weiunpo  36647  copsex2d  37453  relowlssretop  37679  pibt2  37733  heicant  37976  mbfresfi  37987  ftc1anclem6  38019  eqvreltrd  39013  riotasv2d  39403  lcvnbtwn2  39473  lcvnbtwn3  39474  lcvexchlem4  39483  omlfh1N  39704  atlen0  39756  atlatmstc  39765  cvratlem  39867  lnnat  39873  2atlt  39885  athgt  39902  1cvratex  39919  ps-2  39924  llncmp  39968  llncvrlpln  40004  lplncmp  40008  lplncvrlvol  40062  lvolcmp  40063  dalemcea  40106  dalem-cly  40117  dalem10  40119  dalem17  40126  dalem25  40144  dalem38  40156  dalem44  40162  dalem55  40173  2atm2atN  40231  cdlema1N  40237  paddasslem5  40270  dalawlem3  40319  dalawlem7  40323  dalawlem11  40327  dalawlem12  40328  lhp0lt  40449  4atexlemc  40515  cdlemg33a  41152  cdlemg33  41157  cdlemk51  41399  dia2dimlem2  41511  dia2dimlem3  41512  dihmeetlem20N  41772  coprmdvds2d  42440  flt4lem2  43080  flt4lem5f  43090  ismrcd2  43131  pellqrex  43307  jm2.17b  43389  jm2.26lem3  43429  fnwe2lem2  43479  omabs2  43760  addrcom  44901  infxrunb2  45797  0ellimcdiv  46077  dvnprodlem1  46374  stoweidlem15  46443  stoweidlem26  46454  stoweidlem28  46456  stoweidlem32  46460  stoweidlem44  46472  meadjuni  46885  natglobalincr  47305  dfatcolem  47697  icceuelpart  47890  perfectALTVlem1  48191  bgoldbtbndlem2  48276  bgoldbtbndlem3  48277  copisnmnd  48639  assintopass  48684  lcoss  48906  islindeps2  48953  isldepslvec2  48955  isisod  49496  euendfunc  49995