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  3679  ssnelpssd  4048  sotrd  5554  frpomin  6293  fvf1pr  7251  tfisi  7799  tfindsg2  7802  mposn  8042  frxp2  8083  smoord  8294  oelimcl  8525  oeeui  8527  nnawordex  8562  omabs  8576  naddssim  8610  naddel12  8625  ertrd  8649  en2prd  8983  omxpenlem  9005  fodomfir  9227  ixpfi2  9249  supssd  9365  infssd  9396  oismo  9444  cantnflem1c  9597  cantnflem1  9599  cantnflem3  9601  infxpenc2  9933  isfin2-2  10230  axdc2lem  10359  r1limwun  10648  letrd  11292  lelttrd  11293  ltletrd  11295  lttrd  11296  le2subd  11759  ltleaddd  11760  leltaddd  11761  lt2subd  11763  ltmul12a  12000  lemul12ad  12087  lemul12bd  12088  lt2halvesd  12414  uzind  12610  uztrn  12795  xrlttrd  13099  xrlelttrd  13100  xrltletrd  13101  xrletrd  13102  supxrunb1  13260  supxrunb2  13261  ixxun  13303  ixxss1  13305  ixxss2  13306  ixxss12  13307  fldiv4p1lem1div2  13783  fldiv4lem1div2uz2  13784  seqf1o  13994  faclbnd3  14243  relexpindlem  15014  01sqrexlem1  15193  01sqrexlem4  15196  01sqrexlem7  15199  abs3lemd  15415  rlimcn3  15541  o1of2  15564  lo1add  15578  lo1mul  15579  modfsummod  15746  mertenslem1  15838  sin01gt0  16146  cos01gt0  16147  sin02gt0  16148  dvds2addd  16250  dvds2subd  16251  dvdstrd  16253  bezoutlem4  16500  mulgcd  16506  lcmgcdeq  16570  mulgcddvds  16613  rpmulgcd2  16614  rpdvds  16618  divgcdcoprmex  16624  phimullem  16738  eulerthlem1  16740  eulerthlem2  16741  prmdiveq  16745  pythagtriplem4  16779  pcqmul  16813  pcgcd1  16837  pcadd  16849  pockthlem  16865  prmreclem2  16877  4sqlem16  16920  ramub1lem1  16986  ramub1lem2  16987  prmgaplem7  17017  iscatd2  17636  cicsym  17760  initoeu2  17972  joinval  18330  meetval  18344  lattrd  18401  latledi  18432  mulgass  19076  gaorber  19272  psgnunilem4  19461  efgredlem  19711  odadd2  19813  dmdprdpr  20015  ablfacrp2  20033  ablfac1b  20036  ablfac1eu  20039  pgpfac1  20046  orngmul  20831  gsumbagdiaglem  21899  mdetunilem1  22565  mdetunilem4  22568  mdetunilem9  22573  neiptoptop  23084  lmcnp  23257  txcls  23557  txlly  23589  txnlly  23590  tx1stc  23603  alexsubALTlem1  24000  prdsmet  24323  blin2  24382  blcvx  24751  tgqioo  24753  metnrmlem3  24815  iscmet3lem2  25247  ovolmge0  25432  ovolunlem2  25453  mbfi1flimlem  25677  mbfmullem  25680  itg2add  25714  dvferm1lem  25939  dvferm2lem  25941  dvlip2  25950  dvge0  25961  dvcvx  25975  dvfsumabs  25978  ftc1a  25992  plyadd  26170  plymul  26171  dgrlb  26189  plydivlem4  26250  vieta1lem2  26265  ulmdvlem3  26355  sinq12gt0  26459  logdivlti  26572  fsumharmonic  26963  mpodvdsmulf1o  27145  dvdsmulf1o  27147  logfacubnd  27172  perfectlem1  27180  dchrptlem2  27216  2sqlem5  27373  2sqlem8  27377  2sqmod  27387  dchrisum0flblem2  27460  pntibndlem2  27542  pntlemr  27553  pntlemp  27561  nosupbnd1  27666  nosupbnd2lem1  27667  nosupbnd2  27668  noinfbnd1  27681  noinfbnd2lem1  27682  noinfbnd2  27683  noetasuplem4  27688  noetainflem4  27692  ltstrd  27715  ltlestrd  27716  leltstrd  27717  lestrd  27718  oldbdayim  27869  mulsproplem5  28100  mulsproplem6  28101  mulsproplem7  28102  mulsproplem8  28103  ltmulsd  28117  bdayfinbndlem1  28447  bdayfinbnd  28449  axtgpasch  28523  tgjustr  28530  wlkcompim  29688  wwlksnredwwlkn  29951  wwlksnextsurj  29956  upgr4cycl4dv4e  30243  ex-natded5.2-2  30463  chscllem2  31697  chscllem4  31699  nmopge0  31970  nmfnge0  31986  nmoptrii  32153  staddi  32305  stadd3i  32307  atcvatlem  32444  xrofsup  32828  xrge0addgt0  33065  archiabllem2c  33244  linds2eq  33429  ssdifidlprm  33506  lbsdiflsp0  33758  fedgmullem2  33762  esumpmono  34211  unelldsys  34290  omssubaddlem  34431  signstfvneq0  34704  axtgupdim2ALTV  34800  bnj1098  34914  bnj1110  35112  bnj1121  35115  0nn0m1nnn0  35283  cplgredgex  35291  erdszelem8  35368  txsconn  35411  cvmlift2lem10  35482  cvmlift3lem7  35495  dfon2lem6  35956  dfon2lem8  35958  cgrtr4d  36155  cgrtrand  36163  cgrtr3and  36165  cgrextendand  36179  btwnexch3and  36191  btwnexchand  36196  linecgrand  36252  endofsegidand  36256  btwnconn1lem4  36260  btwnconn1lem8  36264  btwnconn1lem11  36267  btwnconn1lem12  36268  brsegle2  36279  seglecgr12im  36280  segleantisym  36285  colinbtwnle  36288  broutsideof2  36292  outsideoftr  36299  outsidele  36302  lineelsb2  36318  linethru  36323  gtinf  36489  weiunpo  36635  copsex2d  37441  relowlssretop  37667  pibt2  37721  heicant  37964  mbfresfi  37975  ftc1anclem6  38007  eqvreltrd  39001  riotasv2d  39391  lcvnbtwn2  39461  lcvnbtwn3  39462  lcvexchlem4  39471  omlfh1N  39692  atlen0  39744  atlatmstc  39753  cvratlem  39855  lnnat  39861  2atlt  39873  athgt  39890  1cvratex  39907  ps-2  39912  llncmp  39956  llncvrlpln  39992  lplncmp  39996  lplncvrlvol  40050  lvolcmp  40051  dalemcea  40094  dalem-cly  40105  dalem10  40107  dalem17  40114  dalem25  40132  dalem38  40144  dalem44  40150  dalem55  40161  2atm2atN  40219  cdlema1N  40225  paddasslem5  40258  dalawlem3  40307  dalawlem7  40311  dalawlem11  40315  dalawlem12  40316  lhp0lt  40437  4atexlemc  40503  cdlemg33a  41140  cdlemg33  41145  cdlemk51  41387  dia2dimlem2  41499  dia2dimlem3  41500  dihmeetlem20N  41760  coprmdvds2d  42428  flt4lem2  43068  flt4lem5f  43078  ismrcd2  43119  pellqrex  43295  jm2.17b  43377  jm2.26lem3  43417  fnwe2lem2  43467  omabs2  43748  addrcom  44889  infxrunb2  45785  0ellimcdiv  46065  dvnprodlem1  46362  stoweidlem15  46431  stoweidlem26  46442  stoweidlem28  46444  stoweidlem32  46448  stoweidlem44  46460  meadjuni  46873  natglobalincr  47295  dfatcolem  47691  icceuelpart  47884  perfectALTVlem1  48185  bgoldbtbndlem2  48270  bgoldbtbndlem3  48271  copisnmnd  48633  assintopass  48678  lcoss  48900  islindeps2  48947  isldepslvec2  48949  isisod  49490  euendfunc  49989