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  3695  ssnelpssd  4068  sotrd  5559  frpomin  6299  fvf1pr  7256  tfisi  7804  tfindsg2  7807  mposn  8048  frxp2  8089  smoord  8300  oelimcl  8531  oeeui  8533  nnawordex  8568  omabs  8582  naddssim  8616  naddel12  8631  ertrd  8655  en2prd  8989  omxpenlem  9011  fodomfir  9233  ixpfi2  9255  supssd  9371  infssd  9402  oismo  9450  cantnflem1c  9601  cantnflem1  9603  cantnflem3  9605  infxpenc2  9937  isfin2-2  10234  axdc2lem  10363  r1limwun  10652  letrd  11295  lelttrd  11296  ltletrd  11298  lttrd  11299  le2subd  11762  ltleaddd  11763  leltaddd  11764  lt2subd  11766  ltmul12a  12002  lemul12ad  12089  lemul12bd  12090  lt2halvesd  12394  uzind  12589  uztrn  12774  xrlttrd  13078  xrlelttrd  13079  xrltletrd  13080  xrletrd  13081  supxrunb1  13239  supxrunb2  13240  ixxun  13282  ixxss1  13284  ixxss2  13285  ixxss12  13286  fldiv4p1lem1div2  13760  fldiv4lem1div2uz2  13761  seqf1o  13971  faclbnd3  14220  relexpindlem  14991  01sqrexlem1  15170  01sqrexlem4  15173  01sqrexlem7  15176  abs3lemd  15392  rlimcn3  15518  o1of2  15541  lo1add  15555  lo1mul  15556  modfsummod  15722  mertenslem1  15812  sin01gt0  16120  cos01gt0  16121  sin02gt0  16122  dvds2addd  16224  dvds2subd  16225  dvdstrd  16227  bezoutlem4  16474  mulgcd  16480  lcmgcdeq  16544  mulgcddvds  16587  rpmulgcd2  16588  rpdvds  16592  divgcdcoprmex  16598  phimullem  16711  eulerthlem1  16713  eulerthlem2  16714  prmdiveq  16718  pythagtriplem4  16752  pcqmul  16786  pcgcd1  16810  pcadd  16822  pockthlem  16838  prmreclem2  16850  4sqlem16  16893  ramub1lem1  16959  ramub1lem2  16960  prmgaplem7  16990  iscatd2  17609  cicsym  17733  initoeu2  17945  joinval  18303  meetval  18317  lattrd  18374  latledi  18405  mulgass  19046  gaorber  19242  psgnunilem4  19431  efgredlem  19681  odadd2  19783  dmdprdpr  19985  ablfacrp2  20003  ablfac1b  20006  ablfac1eu  20009  pgpfac1  20016  orngmul  20803  gsumbagdiaglem  21891  mdetunilem1  22561  mdetunilem4  22564  mdetunilem9  22569  neiptoptop  23080  lmcnp  23253  txcls  23553  txlly  23585  txnlly  23586  tx1stc  23599  alexsubALTlem1  23996  prdsmet  24319  blin2  24378  blcvx  24747  tgqioo  24749  metnrmlem3  24811  iscmet3lem2  25253  ovolmge0  25439  ovolunlem2  25460  mbfi1flimlem  25684  mbfmullem  25687  itg2add  25721  dvferm1lem  25949  dvferm2lem  25951  dvlip2  25961  dvge0  25972  dvcvx  25986  dvfsumabs  25990  ftc1a  26005  plyadd  26183  plymul  26184  dgrlb  26202  plydivlem4  26265  vieta1lem2  26280  ulmdvlem3  26372  sinq12gt0  26477  logdivlti  26590  fsumharmonic  26983  mpodvdsmulf1o  27165  dvdsmulf1o  27167  logfacubnd  27193  perfectlem1  27201  dchrptlem2  27237  2sqlem5  27394  2sqlem8  27398  2sqmod  27408  dchrisum0flblem2  27481  pntibndlem2  27563  pntlemr  27574  pntlemp  27582  nosupbnd1  27687  nosupbnd2lem1  27688  nosupbnd2  27689  noinfbnd1  27702  noinfbnd2lem1  27703  noinfbnd2  27704  noetasuplem4  27709  noetainflem4  27713  ltstrd  27736  ltlestrd  27737  leltstrd  27738  lestrd  27739  oldbdayim  27890  mulsproplem5  28121  mulsproplem6  28122  mulsproplem7  28123  mulsproplem8  28124  ltmulsd  28138  bdayfinbndlem1  28468  bdayfinbnd  28470  axtgpasch  28544  tgjustr  28551  wlkcompim  29710  wwlksnredwwlkn  29973  wwlksnextsurj  29978  upgr4cycl4dv4e  30265  ex-natded5.2-2  30485  chscllem2  31718  chscllem4  31720  nmopge0  31991  nmfnge0  32007  nmoptrii  32174  staddi  32326  stadd3i  32328  atcvatlem  32465  xrofsup  32850  xrge0addgt0  33102  archiabllem2c  33281  linds2eq  33466  ssdifidlprm  33543  lbsdiflsp0  33796  fedgmullem2  33800  esumpmono  34249  unelldsys  34328  omssubaddlem  34469  signstfvneq0  34742  axtgupdim2ALTV  34838  bnj1098  34952  bnj1110  35151  bnj1121  35154  0nn0m1nnn0  35320  cplgredgex  35328  erdszelem8  35405  txsconn  35448  cvmlift2lem10  35519  cvmlift3lem7  35532  dfon2lem6  35993  dfon2lem8  35995  cgrtr4d  36192  cgrtrand  36200  cgrtr3and  36202  cgrextendand  36216  btwnexch3and  36228  btwnexchand  36233  linecgrand  36289  endofsegidand  36293  btwnconn1lem4  36297  btwnconn1lem8  36301  btwnconn1lem11  36304  btwnconn1lem12  36305  brsegle2  36316  seglecgr12im  36317  segleantisym  36322  colinbtwnle  36325  broutsideof2  36329  outsideoftr  36336  outsidele  36339  lineelsb2  36355  linethru  36360  gtinf  36526  weiunpo  36672  copsex2d  37357  relowlssretop  37581  pibt2  37635  heicant  37869  mbfresfi  37880  ftc1anclem6  37912  eqvreltrd  38906  riotasv2d  39296  lcvnbtwn2  39366  lcvnbtwn3  39367  lcvexchlem4  39376  omlfh1N  39597  atlen0  39649  atlatmstc  39658  cvratlem  39760  lnnat  39766  2atlt  39778  athgt  39795  1cvratex  39812  ps-2  39817  llncmp  39861  llncvrlpln  39897  lplncmp  39901  lplncvrlvol  39955  lvolcmp  39956  dalemcea  39999  dalem-cly  40010  dalem10  40012  dalem17  40019  dalem25  40037  dalem38  40049  dalem44  40055  dalem55  40066  2atm2atN  40124  cdlema1N  40130  paddasslem5  40163  dalawlem3  40212  dalawlem7  40216  dalawlem11  40220  dalawlem12  40221  lhp0lt  40342  4atexlemc  40408  cdlemg33a  41045  cdlemg33  41050  cdlemk51  41292  dia2dimlem2  41404  dia2dimlem3  41405  dihmeetlem20N  41665  coprmdvds2d  42334  flt4lem2  42968  flt4lem5f  42978  ismrcd2  43019  pellqrex  43199  jm2.17b  43281  jm2.26lem3  43321  fnwe2lem2  43371  omabs2  43652  addrcom  44793  infxrunb2  45689  0ellimcdiv  45970  dvnprodlem1  46267  stoweidlem15  46336  stoweidlem26  46347  stoweidlem28  46349  stoweidlem32  46353  stoweidlem44  46365  meadjuni  46778  natglobalincr  47198  dfatcolem  47578  icceuelpart  47759  perfectALTVlem1  48044  bgoldbtbndlem2  48129  bgoldbtbndlem3  48130  copisnmnd  48492  assintopass  48537  lcoss  48759  islindeps2  48806  isldepslvec2  48808  isisod  49349  euendfunc  49848