Theorem mp2and 706

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

Syntax hints:   → wi 4   ∧ wa 397

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 209  df-an 398

This theorem is referenced by:  reu2eqd  3678  ssnelpssd  4048  sotrd  5554  frpomin  6294  fvf1pr  7254  tfisi  7802  tfindsg2  7805  mposn  8044  frxp2  8086  smoord  8298  oelimcl  8530  oeeui  8532  nnawordex  8567  omabs  8581  naddssim  8615  naddel12  8630  ertrd  8654  en2prd  8988  omxpenlem  9010  fodomfir  9232  ixpfi2  9254  supssd  9370  infssd  9401  oismo  9449  cantnflem1c  9603  cantnflem1  9605  cantnflem3  9607  infxpenc2  9939  isfin2-2  10237  axdc2lem  10366  r1limwun  10655  letrd  11299  lelttrd  11300  ltletrd  11302  lttrd  11303  le2subd  11766  ltleaddd  11767  leltaddd  11768  lt2subd  11770  ltmul12a  12006  lemul12ad  12093  lemul12bd  12094  lt2halvesd  12420  uzind  12616  uztrn  12801  xrlttrd  13105  xrlelttrd  13106  xrltletrd  13107  xrletrd  13108  supxrunb1  13266  supxrunb2  13267  ixxun  13309  ixxss1  13311  ixxss2  13312  ixxss12  13313  fldiv4p1lem1div2  13789  fldiv4lem1div2uz2  13790  seqf1o  14000  faclbnd3  14249  relexpindlem  15020  01sqrexlem1  15199  01sqrexlem4  15202  01sqrexlem7  15205  abs3lemd  15421  rlimcn3  15547  o1of2  15570  lo1add  15584  lo1mul  15585  modfsummod  15752  mertenslem1  15844  sin01gt0  16152  cos01gt0  16153  sin02gt0  16154  dvds2addd  16256  dvds2subd  16257  dvdstrd  16259  bezoutlem4  16506  mulgcd  16512  lcmgcdeq  16576  mulgcddvds  16619  rpmulgcd2  16620  rpdvds  16624  divgcdcoprmex  16630  phimullem  16744  eulerthlem1  16746  eulerthlem2  16747  prmdiveq  16751  pythagtriplem4  16785  pcqmul  16819  pcgcd1  16843  pcadd  16855  pockthlem  16871  prmreclem2  16883  4sqlem16  16926  ramub1lem1  16992  ramub1lem2  16993  prmgaplem7  17023  iscatd2  17642  cicsym  17766  initoeu2  17978  joinval  18336  meetval  18350  lattrd  18407  latledi  18438  mulgass  19082  gaorber  19277  psgnunilem4  19466  efgredlem  19716  odadd2  19818  dmdprdpr  20020  ablfacrp2  20038  ablfac1b  20041  ablfac1eu  20044  pgpfac1  20051  orngmul  20840  gsumbagdiaglem  21909  mdetunilem1  22598  mdetunilem4  22601  mdetunilem9  22606  neiptoptop  23117  lmcnp  23290  txcls  23590  txlly  23622  txnlly  23623  tx1stc  23636  alexsubALTlem1  24033  prdsmet  24356  blin2  24415  blcvx  24784  tgqioo  24786  metnrmlem3  24848  iscmet3lem2  25280  ovolmge0  25465  ovolunlem2  25486  mbfi1flimlem  25710  mbfmullem  25713  itg2add  25747  dvferm1lem  25972  dvferm2lem  25974  dvlip2  25983  dvge0  25994  dvcvx  26008  dvfsumabs  26011  ftc1a  26025  plyadd  26203  plymul  26204  dgrlb  26222  plydivlem4  26283  vieta1lem2  26298  ulmdvlem3  26388  sinq12gt0  26492  logdivlti  26605  fsumharmonic  26996  mpodvdsmulf1o  27178  dvdsmulf1o  27180  logfacubnd  27205  perfectlem1  27213  dchrptlem2  27249  2sqlem5  27406  2sqlem8  27410  2sqmod  27420  dchrisum0flblem2  27493  pntibndlem2  27575  pntlemr  27586  pntlemp  27594  nosupbnd1  27698  nosupbnd2lem1  27699  nosupbnd2  27700  noinfbnd1  27713  noinfbnd2lem1  27714  noinfbnd2  27715  noetasuplem4  27720  noetainflem4  27724  ltstrd  27747  ltlestrd  27748  leltstrd  27749  lestrd  27750  oldbdayim  27901  mulsproplem5  28132  mulsproplem6  28133  mulsproplem7  28134  mulsproplem8  28135  ltmulsd  28149  bdayfinbndlem1  28479  bdayfinbnd  28481  axtgpasch  28555  tgjustr  28562  wlkcompim  29720  wwlksnredwwlkn  29983  wwlksnextsurj  29988  upgr4cycl4dv4e  30275  ex-natded5.2-2  30495  chscllem2  31729  chscllem4  31731  nmopge0  32002  nmfnge0  32018  nmoptrii  32185  staddi  32337  stadd3i  32339  atcvatlem  32476  xrofsup  32861  xrge0addgt0  33098  archiabllem2c  33278  linds2eq  33466  ssdifidlprm  33543  lbsdiflsp0  33820  fedgmullem2  33824  esumpmono  34273  unelldsys  34352  omssubaddlem  34493  signstfvneq0  34766  axtgupdim2ALTV  34862  bnj1098  34979  bnj1110  35177  bnj1121  35180  0nn0m1nnn0  35354  cplgredgex  35362  erdszelem8  35439  txsconn  35482  cvmlift2lem10  35553  cvmlift3lem7  35566  dfon2lem6  36027  dfon2lem8  36029  cgrtr4d  36226  cgrtrand  36234  cgrtr3and  36236  cgrextendand  36250  btwnexch3and  36262  btwnexchand  36267  linecgrand  36323  endofsegidand  36327  btwnconn1lem4  36331  btwnconn1lem8  36335  btwnconn1lem11  36338  btwnconn1lem12  36339  brsegle2  36350  seglecgr12im  36351  segleantisym  36356  colinbtwnle  36359  broutsideof2  36363  outsideoftr  36370  outsidele  36373  lineelsb2  36389  linethru  36394  gtinf  36560  weiunpo  36706  copsex2d  37512  relowlssretop  37738  pibt2  37792  heicant  38035  mbfresfi  38046  ftc1anclem6  38078  eqvreltrd  39072  riotasv2d  39462  lcvnbtwn2  39532  lcvnbtwn3  39533  lcvexchlem4  39542  omlfh1N  39763  atlen0  39815  atlatmstc  39824  cvratlem  39926  lnnat  39932  2atlt  39944  athgt  39961  1cvratex  39978  ps-2  39983  llncmp  40027  llncvrlpln  40063  lplncmp  40067  lplncvrlvol  40121  lvolcmp  40122  dalemcea  40165  dalem-cly  40176  dalem10  40178  dalem17  40185  dalem25  40203  dalem38  40215  dalem44  40221  dalem55  40232  2atm2atN  40290  cdlema1N  40296  paddasslem5  40329  dalawlem3  40378  dalawlem7  40382  dalawlem11  40386  dalawlem12  40387  lhp0lt  40508  4atexlemc  40574  cdlemg33a  41211  cdlemg33  41216  cdlemk51  41458  dia2dimlem2  41570  dia2dimlem3  41571  dihmeetlem20N  41831  coprmdvds2d  42499  flt4lem2  43110  flt4lem5f  43120  ismrcd2  43161  pellqrex  43337  jm2.17b  43419  jm2.26lem3  43459  fnwe2lem2  43509  omabs2  43790  addrcom  44931  infxrunb2  45824  0ellimcdiv  46104  dvnprodlem1  46401  stoweidlem15  46470  stoweidlem26  46481  stoweidlem28  46483  stoweidlem32  46487  stoweidlem44  46499  meadjuni  46912  natglobalincr  47334  dfatcolem  47730  icceuelpart  47923  perfectALTVlem1  48224  bgoldbtbndlem2  48309  bgoldbtbndlem3  48310  copisnmnd  48672  assintopass  48717  lcoss  48939  islindeps2  48986  isldepslvec2  48988  isisod  49529  euendfunc  50028