Theorem mp2and 699

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 695	. 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  3707  ssnelpssd  4078  sotrd  5572  frpomin  6313  fvf1pr  7282  tfisi  7835  tfindsg2  7838  mposn  8082  frxp2  8123  smoord  8334  oelimcl  8564  oeeui  8566  nnawordex  8601  omabs  8615  naddssim  8649  naddel12  8664  ertrd  8687  en2prd  9019  omxpenlem  9042  fodomfir  9279  ixpfi2  9301  supssd  9414  infssd  9445  oismo  9493  cantnflem1c  9640  cantnflem1  9642  cantnflem3  9644  infxpenc2  9975  isfin2-2  10272  axdc2lem  10401  r1limwun  10689  letrd  11331  lelttrd  11332  ltletrd  11334  lttrd  11335  le2subd  11798  ltleaddd  11799  leltaddd  11800  lt2subd  11802  ltmul12a  12038  lemul12ad  12125  lemul12bd  12126  lt2halvesd  12430  uzind  12626  uztrn  12811  xrlttrd  13119  xrlelttrd  13120  xrltletrd  13121  xrletrd  13122  supxrunb1  13279  supxrunb2  13280  ixxun  13322  ixxss1  13324  ixxss2  13325  ixxss12  13326  fldiv4p1lem1div2  13797  fldiv4lem1div2uz2  13798  seqf1o  14008  faclbnd3  14257  relexpindlem  15029  01sqrexlem1  15208  01sqrexlem4  15211  01sqrexlem7  15214  abs3lemd  15430  rlimcn3  15556  o1of2  15579  lo1add  15593  lo1mul  15594  modfsummod  15760  mertenslem1  15850  sin01gt0  16158  cos01gt0  16159  sin02gt0  16160  dvds2addd  16262  dvds2subd  16263  dvdstrd  16265  bezoutlem4  16512  mulgcd  16518  lcmgcdeq  16582  mulgcddvds  16625  rpmulgcd2  16626  rpdvds  16630  divgcdcoprmex  16636  phimullem  16749  eulerthlem1  16751  eulerthlem2  16752  prmdiveq  16756  pythagtriplem4  16790  pcqmul  16824  pcgcd1  16848  pcadd  16860  pockthlem  16876  prmreclem2  16888  4sqlem16  16931  ramub1lem1  16997  ramub1lem2  16998  prmgaplem7  17028  iscatd2  17642  cicsym  17766  initoeu2  17978  joinval  18336  meetval  18350  lattrd  18405  latledi  18436  mulgass  19043  gaorber  19240  psgnunilem4  19427  efgredlem  19677  odadd2  19779  dmdprdpr  19981  ablfacrp2  19999  ablfac1b  20002  ablfac1eu  20005  pgpfac1  20012  gsumbagdiaglem  21839  mdetunilem1  22499  mdetunilem4  22502  mdetunilem9  22507  neiptoptop  23018  lmcnp  23191  txcls  23491  txlly  23523  txnlly  23524  tx1stc  23537  alexsubALTlem1  23934  prdsmet  24258  blin2  24317  blcvx  24686  tgqioo  24688  metnrmlem3  24750  iscmet3lem2  25192  ovolmge0  25378  ovolunlem2  25399  mbfi1flimlem  25623  mbfmullem  25626  itg2add  25660  dvferm1lem  25888  dvferm2lem  25890  dvlip2  25900  dvge0  25911  dvcvx  25925  dvfsumabs  25929  ftc1a  25944  plyadd  26122  plymul  26123  dgrlb  26141  plydivlem4  26204  vieta1lem2  26219  ulmdvlem3  26311  sinq12gt0  26416  logdivlti  26529  fsumharmonic  26922  mpodvdsmulf1o  27104  dvdsmulf1o  27106  logfacubnd  27132  perfectlem1  27140  dchrptlem2  27176  2sqlem5  27333  2sqlem8  27337  2sqmod  27347  dchrisum0flblem2  27420  pntibndlem2  27502  pntlemr  27513  pntlemp  27521  nosupbnd1  27626  nosupbnd2lem1  27627  nosupbnd2  27628  noinfbnd1  27641  noinfbnd2lem1  27642  noinfbnd2  27643  noetasuplem4  27648  noetainflem4  27652  slttrd  27671  sltletrd  27672  slelttrd  27673  sletrd  27674  oldbdayim  27800  mulsproplem5  28023  mulsproplem6  28024  mulsproplem7  28025  mulsproplem8  28026  sltmuld  28040  axtgpasch  28394  tgjustr  28401  wlkcompim  29560  wwlksnredwwlkn  29825  wwlksnextsurj  29830  upgr4cycl4dv4e  30114  ex-natded5.2-2  30334  chscllem2  31567  chscllem4  31569  nmopge0  31840  nmfnge0  31856  nmoptrii  32023  staddi  32175  stadd3i  32177  atcvatlem  32314  xrofsup  32690  xrge0addgt0  32958  archiabllem2c  33149  orngmul  33281  linds2eq  33352  ssdifidlprm  33429  lbsdiflsp0  33622  fedgmullem2  33626  esumpmono  34069  unelldsys  34148  omssubaddlem  34290  signstfvneq0  34563  axtgupdim2ALTV  34659  bnj1098  34773  bnj1110  34972  bnj1121  34975  0nn0m1nnn0  35100  cplgredgex  35108  erdszelem8  35185  txsconn  35228  cvmlift2lem10  35299  cvmlift3lem7  35312  dfon2lem6  35776  dfon2lem8  35778  cgrtr4d  35973  cgrtrand  35981  cgrtr3and  35983  cgrextendand  35997  btwnexch3and  36009  btwnexchand  36014  linecgrand  36070  endofsegidand  36074  btwnconn1lem4  36078  btwnconn1lem8  36082  btwnconn1lem11  36085  btwnconn1lem12  36086  brsegle2  36097  seglecgr12im  36098  segleantisym  36103  colinbtwnle  36106  broutsideof2  36110  outsideoftr  36117  outsidele  36120  lineelsb2  36136  linethru  36141  gtinf  36307  weiunpo  36453  copsex2d  37127  relowlssretop  37351  pibt2  37405  heicant  37649  mbfresfi  37660  ftc1anclem6  37692  eqvreltrd  38599  riotasv2d  38950  lcvnbtwn2  39020  lcvnbtwn3  39021  lcvexchlem4  39030  omlfh1N  39251  atlen0  39303  atlatmstc  39312  cvratlem  39415  lnnat  39421  2atlt  39433  athgt  39450  1cvratex  39467  ps-2  39472  llncmp  39516  llncvrlpln  39552  lplncmp  39556  lplncvrlvol  39610  lvolcmp  39611  dalemcea  39654  dalem-cly  39665  dalem10  39667  dalem17  39674  dalem25  39692  dalem38  39704  dalem44  39710  dalem55  39721  2atm2atN  39779  cdlema1N  39785  paddasslem5  39818  dalawlem3  39867  dalawlem7  39871  dalawlem11  39875  dalawlem12  39876  lhp0lt  39997  4atexlemc  40063  cdlemg33a  40700  cdlemg33  40705  cdlemk51  40947  dia2dimlem2  41059  dia2dimlem3  41060  dihmeetlem20N  41320  coprmdvds2d  41989  flt4lem2  42635  flt4lem5f  42645  ismrcd2  42687  pellqrex  42867  jm2.17b  42950  jm2.26lem3  42990  fnwe2lem2  43040  omabs2  43321  addrcom  44464  infxrunb2  45364  0ellimcdiv  45647  dvnprodlem1  45944  stoweidlem15  46013  stoweidlem26  46024  stoweidlem28  46026  stoweidlem32  46030  stoweidlem44  46042  meadjuni  46455  natglobalincr  46875  dfatcolem  47256  icceuelpart  47437  perfectALTVlem1  47722  bgoldbtbndlem2  47807  bgoldbtbndlem3  47808  copisnmnd  48157  assintopass  48202  lcoss  48425  islindeps2  48472  isldepslvec2  48474  isisod  49016  euendfunc  49515