Theorem mp2and 697

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  reu2eqd  3729  ssnelpssd  4109  frpomin  6346  tfisi  7862  tfindsg2  7865  mposn  8106  frxp2  8147  smoord  8384  oelimcl  8619  oeeui  8621  nnawordex  8656  omabs  8670  naddssim  8704  naddel12  8719  ertrd  8739  en2prd  9071  omxpenlem  9096  ixpfi2  9374  oismo  9563  cantnflem1c  9710  cantnflem1  9712  cantnflem3  9714  infxpenc2  10045  isfin2-2  10342  axdc2lem  10471  r1limwun  10759  letrd  11401  lelttrd  11402  ltletrd  11404  lttrd  11405  le2addd  11863  le2subd  11864  ltleaddd  11865  leltaddd  11866  lt2subd  11868  ltmul12a  12100  lemul12ad  12186  lemul12bd  12187  lt2halvesd  12490  uzind  12684  uztrn  12870  xrlttrd  13170  xrlelttrd  13171  xrltletrd  13172  xrletrd  13173  supxrunb1  13330  supxrunb2  13331  ixxun  13372  ixxss1  13374  ixxss2  13375  ixxss12  13376  fldiv4p1lem1div2  13833  fldiv4lem1div2uz2  13834  seqf1o  14041  faclbnd3  14284  relexpindlem  15043  01sqrexlem1  15222  01sqrexlem4  15225  01sqrexlem7  15228  abs3lemd  15441  rlimcn3  15567  o1of2  15590  lo1add  15604  lo1mul  15605  modfsummod  15773  mertenslem1  15863  sin01gt0  16167  cos01gt0  16168  sin02gt0  16169  dvds2addd  16269  dvds2subd  16270  dvdstrd  16272  bezoutlem4  16518  mulgcd  16524  lcmgcdeq  16583  mulgcddvds  16626  rpmulgcd2  16627  rpdvds  16631  divgcdcoprmex  16637  phimullem  16748  eulerthlem1  16750  eulerthlem2  16751  prmdiveq  16755  pythagtriplem4  16788  pcqmul  16822  pcgcd1  16846  pcadd  16858  pockthlem  16874  prmreclem2  16886  4sqlem16  16929  ramub1lem1  16995  ramub1lem2  16996  prmgaplem7  17026  iscatd2  17661  cicsym  17787  initoeu2  18005  joinval  18369  meetval  18383  lattrd  18438  latledi  18469  mulgass  19071  gaorber  19264  psgnunilem4  19457  efgredlem  19707  odadd2  19809  dmdprdpr  20011  ablfacrp2  20029  ablfac1b  20032  ablfac1eu  20035  pgpfac1  20042  gsumbagdiaglemOLD  21877  gsumbagdiaglem  21880  mdetunilem1  22545  mdetunilem4  22548  mdetunilem9  22553  neiptoptop  23066  lmcnp  23239  txcls  23539  txlly  23571  txnlly  23572  tx1stc  23585  alexsubALTlem1  23982  prdsmet  24307  blin2  24366  blcvx  24745  tgqioo  24747  metnrmlem3  24808  iscmet3lem2  25251  ovolmge0  25437  ovolunlem2  25458  mbfi1flimlem  25683  mbfmullem  25686  itg2add  25720  dvferm1lem  25947  dvferm2lem  25949  dvlip2  25959  dvge0  25970  dvcvx  25984  dvfsumabs  25988  ftc1a  26003  plyadd  26182  plymul  26183  dgrlb  26201  plydivlem4  26262  vieta1lem2  26277  ulmdvlem3  26369  sinq12gt0  26473  logdivlti  26585  fsumharmonic  26975  mpodvdsmulf1o  27157  dvdsmulf1o  27159  logfacubnd  27185  perfectlem1  27193  dchrptlem2  27229  2sqlem5  27386  2sqlem8  27390  2sqmod  27400  dchrisum0flblem2  27473  pntibndlem2  27555  pntlemr  27566  pntlemp  27574  nosupbnd1  27678  nosupbnd2lem1  27679  nosupbnd2  27680  noinfbnd1  27693  noinfbnd2lem1  27694  noinfbnd2  27695  noetasuplem4  27700  noetainflem4  27704  slttrd  27723  sltletrd  27724  slelttrd  27725  sletrd  27726  oldbdayim  27846  mulsproplem5  28055  mulsproplem6  28056  mulsproplem7  28057  mulsproplem8  28058  sltmuld  28072  axtgpasch  28328  tgjustr  28335  wlkcompim  29503  wwlksnredwwlkn  29763  wwlksnextsurj  29768  upgr4cycl4dv4e  30052  ex-natded5.2-2  30272  chscllem2  31505  chscllem4  31507  nmopge0  31778  nmfnge0  31794  nmoptrii  31961  staddi  32113  stadd3i  32115  atcvatlem  32252  supssd  32552  infssd  32553  xrofsup  32598  xrge0addgt0  32813  archiabllem2c  32971  orngmul  33089  linds2eq  33164  lbsdiflsp0  33411  fedgmullem2  33415  esumpmono  33785  unelldsys  33864  omssubaddlem  34006  signstfvneq0  34291  axtgupdim2ALTV  34387  bnj1098  34501  bnj1110  34700  bnj1121  34703  0nn0m1nnn0  34809  cplgredgex  34817  erdszelem8  34895  txsconn  34938  cvmlift2lem10  35009  cvmlift3lem7  35022  sotrd  35446  dfon2lem6  35471  dfon2lem8  35473  cgrtr4d  35668  cgrtrand  35676  cgrtr3and  35678  cgrextendand  35692  btwnexch3and  35704  btwnexchand  35709  linecgrand  35765  endofsegidand  35769  btwnconn1lem4  35773  btwnconn1lem8  35777  btwnconn1lem11  35780  btwnconn1lem12  35781  brsegle2  35792  seglecgr12im  35793  segleantisym  35798  colinbtwnle  35801  broutsideof2  35805  outsideoftr  35812  outsidele  35815  lineelsb2  35831  linethru  35836  gtinf  35890  copsex2d  36705  relowlssretop  36929  pibt2  36983  heicant  37215  mbfresfi  37226  ftc1anclem6  37258  eqvreltrd  38166  riotasv2d  38515  lcvnbtwn2  38585  lcvnbtwn3  38586  lcvexchlem4  38595  omlfh1N  38816  atlen0  38868  atlatmstc  38877  cvratlem  38980  lnnat  38986  2atlt  38998  athgt  39015  1cvratex  39032  ps-2  39037  llncmp  39081  llncvrlpln  39117  lplncmp  39121  lplncvrlvol  39175  lvolcmp  39176  dalemcea  39219  dalem-cly  39230  dalem10  39232  dalem17  39239  dalem25  39257  dalem38  39269  dalem44  39275  dalem55  39286  2atm2atN  39344  cdlema1N  39350  paddasslem5  39383  dalawlem3  39432  dalawlem7  39436  dalawlem11  39440  dalawlem12  39441  lhp0lt  39562  4atexlemc  39628  cdlemg33a  40265  cdlemg33  40270  cdlemk51  40512  dia2dimlem2  40624  dia2dimlem3  40625  dihmeetlem20N  40885  coprmdvds2d  41558  flt4lem2  42153  flt4lem5f  42163  ismrcd2  42201  pellqrex  42381  jm2.17b  42464  jm2.26lem3  42504  fnwe2lem2  42557  omabs2  42843  addrcom  43994  infxrunb2  44830  0ellimcdiv  45117  stoweidlem15  45483  stoweidlem26  45494  stoweidlem28  45496  stoweidlem32  45500  stoweidlem44  45512  meadjuni  45925  natglobalincr  46343  dfatcolem  46715  icceuelpart  46855  perfectALTVlem1  47140  bgoldbtbndlem2  47225  bgoldbtbndlem3  47226  copisnmnd  47359  assintopass  47404  lcoss  47632  islindeps2  47679  isldepslvec2  47681  difmodm1lt  47723