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  5556  frpomin  6296  fvf1pr  7253  tfisi  7801  tfindsg2  7804  mposn  8044  frxp2  8085  smoord  8296  oelimcl  8527  oeeui  8529  nnawordex  8564  omabs  8578  naddssim  8612  naddel12  8627  ertrd  8651  en2prd  8985  omxpenlem  9007  fodomfir  9229  ixpfi2  9251  supssd  9367  infssd  9398  oismo  9446  cantnflem1c  9597  cantnflem1  9599  cantnflem3  9601  infxpenc2  9933  isfin2-2  10230  axdc2lem  10359  r1limwun  10648  letrd  11291  lelttrd  11292  ltletrd  11294  lttrd  11295  le2subd  11758  ltleaddd  11759  leltaddd  11760  lt2subd  11762  ltmul12a  11998  lemul12ad  12085  lemul12bd  12086  lt2halvesd  12390  uzind  12585  uztrn  12770  xrlttrd  13074  xrlelttrd  13075  xrltletrd  13076  xrletrd  13077  supxrunb1  13235  supxrunb2  13236  ixxun  13278  ixxss1  13280  ixxss2  13281  ixxss12  13282  fldiv4p1lem1div2  13756  fldiv4lem1div2uz2  13757  seqf1o  13967  faclbnd3  14216  relexpindlem  14987  01sqrexlem1  15166  01sqrexlem4  15169  01sqrexlem7  15172  abs3lemd  15388  rlimcn3  15514  o1of2  15537  lo1add  15551  lo1mul  15552  modfsummod  15718  mertenslem1  15808  sin01gt0  16116  cos01gt0  16117  sin02gt0  16118  dvds2addd  16220  dvds2subd  16221  dvdstrd  16223  bezoutlem4  16470  mulgcd  16476  lcmgcdeq  16540  mulgcddvds  16583  rpmulgcd2  16584  rpdvds  16588  divgcdcoprmex  16594  phimullem  16707  eulerthlem1  16709  eulerthlem2  16710  prmdiveq  16714  pythagtriplem4  16748  pcqmul  16782  pcgcd1  16806  pcadd  16818  pockthlem  16834  prmreclem2  16846  4sqlem16  16889  ramub1lem1  16955  ramub1lem2  16956  prmgaplem7  16986  iscatd2  17605  cicsym  17729  initoeu2  17941  joinval  18299  meetval  18313  lattrd  18370  latledi  18401  mulgass  19045  gaorber  19241  psgnunilem4  19430  efgredlem  19680  odadd2  19782  dmdprdpr  19984  ablfacrp2  20002  ablfac1b  20005  ablfac1eu  20008  pgpfac1  20015  orngmul  20800  gsumbagdiaglem  21887  mdetunilem1  22555  mdetunilem4  22558  mdetunilem9  22563  neiptoptop  23074  lmcnp  23247  txcls  23547  txlly  23579  txnlly  23580  tx1stc  23593  alexsubALTlem1  23990  prdsmet  24313  blin2  24372  blcvx  24741  tgqioo  24743  metnrmlem3  24805  iscmet3lem2  25237  ovolmge0  25422  ovolunlem2  25443  mbfi1flimlem  25667  mbfmullem  25670  itg2add  25704  dvferm1lem  25929  dvferm2lem  25931  dvlip2  25941  dvge0  25952  dvcvx  25966  dvfsumabs  25970  ftc1a  25985  plyadd  26163  plymul  26164  dgrlb  26182  plydivlem4  26244  vieta1lem2  26259  ulmdvlem3  26351  sinq12gt0  26456  logdivlti  26569  fsumharmonic  26962  mpodvdsmulf1o  27144  dvdsmulf1o  27146  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  29689  wwlksnredwwlkn  29952  wwlksnextsurj  29957  upgr4cycl4dv4e  30244  ex-natded5.2-2  30464  chscllem2  31698  chscllem4  31700  nmopge0  31971  nmfnge0  31987  nmoptrii  32154  staddi  32306  stadd3i  32308  atcvatlem  32445  xrofsup  32830  xrge0addgt0  33082  archiabllem2c  33261  linds2eq  33446  ssdifidlprm  33523  lbsdiflsp0  33776  fedgmullem2  33780  esumpmono  34229  unelldsys  34308  omssubaddlem  34449  signstfvneq0  34722  axtgupdim2ALTV  34818  bnj1098  34932  bnj1110  35130  bnj1121  35133  0nn0m1nnn0  35301  cplgredgex  35309  erdszelem8  35386  txsconn  35429  cvmlift2lem10  35500  cvmlift3lem7  35513  dfon2lem6  35974  dfon2lem8  35976  cgrtr4d  36173  cgrtrand  36181  cgrtr3and  36183  cgrextendand  36197  btwnexch3and  36209  btwnexchand  36214  linecgrand  36270  endofsegidand  36274  btwnconn1lem4  36278  btwnconn1lem8  36282  btwnconn1lem11  36285  btwnconn1lem12  36286  brsegle2  36297  seglecgr12im  36298  segleantisym  36303  colinbtwnle  36306  broutsideof2  36310  outsideoftr  36317  outsidele  36320  lineelsb2  36336  linethru  36341  gtinf  36507  weiunpo  36653  copsex2d  37451  relowlssretop  37675  pibt2  37729  heicant  37967  mbfresfi  37978  ftc1anclem6  38010  eqvreltrd  39004  riotasv2d  39394  lcvnbtwn2  39464  lcvnbtwn3  39465  lcvexchlem4  39474  omlfh1N  39695  atlen0  39747  atlatmstc  39756  cvratlem  39858  lnnat  39864  2atlt  39876  athgt  39893  1cvratex  39910  ps-2  39915  llncmp  39959  llncvrlpln  39995  lplncmp  39999  lplncvrlvol  40053  lvolcmp  40054  dalemcea  40097  dalem-cly  40108  dalem10  40110  dalem17  40117  dalem25  40135  dalem38  40147  dalem44  40153  dalem55  40164  2atm2atN  40222  cdlema1N  40228  paddasslem5  40261  dalawlem3  40310  dalawlem7  40314  dalawlem11  40318  dalawlem12  40319  lhp0lt  40440  4atexlemc  40506  cdlemg33a  41143  cdlemg33  41148  cdlemk51  41390  dia2dimlem2  41502  dia2dimlem3  41503  dihmeetlem20N  41763  coprmdvds2d  42432  flt4lem2  43079  flt4lem5f  43089  ismrcd2  43130  pellqrex  43310  jm2.17b  43392  jm2.26lem3  43432  fnwe2lem2  43482  omabs2  43763  addrcom  44904  infxrunb2  45800  0ellimcdiv  46081  dvnprodlem1  46378  stoweidlem15  46447  stoweidlem26  46458  stoweidlem28  46460  stoweidlem32  46464  stoweidlem44  46476  meadjuni  46889  natglobalincr  47309  dfatcolem  47689  icceuelpart  47870  perfectALTVlem1  48155  bgoldbtbndlem2  48240  bgoldbtbndlem3  48241  copisnmnd  48603  assintopass  48648  lcoss  48870  islindeps2  48917  isldepslvec2  48919  isisod  49460  euendfunc  49959