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  3719  ssnelpssd  4090  sotrd  5587  frpomin  6329  fvf1pr  7300  tfisi  7854  tfindsg2  7857  mposn  8102  frxp2  8143  smoord  8379  oelimcl  8612  oeeui  8614  nnawordex  8649  omabs  8663  naddssim  8697  naddel12  8712  ertrd  8735  en2prd  9062  omxpenlem  9087  fodomfir  9340  ixpfi2  9362  supssd  9475  infssd  9506  oismo  9554  cantnflem1c  9701  cantnflem1  9703  cantnflem3  9705  infxpenc2  10036  isfin2-2  10333  axdc2lem  10462  r1limwun  10750  letrd  11392  lelttrd  11393  ltletrd  11395  lttrd  11396  le2subd  11857  ltleaddd  11858  leltaddd  11859  lt2subd  11861  ltmul12a  12097  lemul12ad  12184  lemul12bd  12185  lt2halvesd  12489  uzind  12685  uztrn  12870  xrlttrd  13175  xrlelttrd  13176  xrltletrd  13177  xrletrd  13178  supxrunb1  13335  supxrunb2  13336  ixxun  13378  ixxss1  13380  ixxss2  13381  ixxss12  13382  fldiv4p1lem1div2  13852  fldiv4lem1div2uz2  13853  seqf1o  14061  faclbnd3  14310  relexpindlem  15082  01sqrexlem1  15261  01sqrexlem4  15264  01sqrexlem7  15267  abs3lemd  15480  rlimcn3  15606  o1of2  15629  lo1add  15643  lo1mul  15644  modfsummod  15810  mertenslem1  15900  sin01gt0  16208  cos01gt0  16209  sin02gt0  16210  dvds2addd  16311  dvds2subd  16312  dvdstrd  16314  bezoutlem4  16561  mulgcd  16567  lcmgcdeq  16631  mulgcddvds  16674  rpmulgcd2  16675  rpdvds  16679  divgcdcoprmex  16685  phimullem  16798  eulerthlem1  16800  eulerthlem2  16801  prmdiveq  16805  pythagtriplem4  16839  pcqmul  16873  pcgcd1  16897  pcadd  16909  pockthlem  16925  prmreclem2  16937  4sqlem16  16980  ramub1lem1  17046  ramub1lem2  17047  prmgaplem7  17077  iscatd2  17693  cicsym  17817  initoeu2  18029  joinval  18387  meetval  18401  lattrd  18456  latledi  18487  mulgass  19094  gaorber  19291  psgnunilem4  19478  efgredlem  19728  odadd2  19830  dmdprdpr  20032  ablfacrp2  20050  ablfac1b  20053  ablfac1eu  20056  pgpfac1  20063  gsumbagdiaglem  21890  mdetunilem1  22550  mdetunilem4  22553  mdetunilem9  22558  neiptoptop  23069  lmcnp  23242  txcls  23542  txlly  23574  txnlly  23575  tx1stc  23588  alexsubALTlem1  23985  prdsmet  24309  blin2  24368  blcvx  24737  tgqioo  24739  metnrmlem3  24801  iscmet3lem2  25244  ovolmge0  25430  ovolunlem2  25451  mbfi1flimlem  25675  mbfmullem  25678  itg2add  25712  dvferm1lem  25940  dvferm2lem  25942  dvlip2  25952  dvge0  25963  dvcvx  25977  dvfsumabs  25981  ftc1a  25996  plyadd  26174  plymul  26175  dgrlb  26193  plydivlem4  26256  vieta1lem2  26271  ulmdvlem3  26363  sinq12gt0  26468  logdivlti  26581  fsumharmonic  26974  mpodvdsmulf1o  27156  dvdsmulf1o  27158  logfacubnd  27184  perfectlem1  27192  dchrptlem2  27228  2sqlem5  27385  2sqlem8  27389  2sqmod  27399  dchrisum0flblem2  27472  pntibndlem2  27554  pntlemr  27565  pntlemp  27573  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  27852  mulsproplem5  28075  mulsproplem6  28076  mulsproplem7  28077  mulsproplem8  28078  sltmuld  28092  axtgpasch  28446  tgjustr  28453  wlkcompim  29612  wwlksnredwwlkn  29877  wwlksnextsurj  29882  upgr4cycl4dv4e  30166  ex-natded5.2-2  30386  chscllem2  31619  chscllem4  31621  nmopge0  31892  nmfnge0  31908  nmoptrii  32075  staddi  32227  stadd3i  32229  atcvatlem  32366  xrofsup  32744  xrge0addgt0  33012  archiabllem2c  33193  orngmul  33325  linds2eq  33396  ssdifidlprm  33473  lbsdiflsp0  33666  fedgmullem2  33670  esumpmono  34110  unelldsys  34189  omssubaddlem  34331  signstfvneq0  34604  axtgupdim2ALTV  34700  bnj1098  34814  bnj1110  35013  bnj1121  35016  0nn0m1nnn0  35135  cplgredgex  35143  erdszelem8  35220  txsconn  35263  cvmlift2lem10  35334  cvmlift3lem7  35347  dfon2lem6  35806  dfon2lem8  35808  cgrtr4d  36003  cgrtrand  36011  cgrtr3and  36013  cgrextendand  36027  btwnexch3and  36039  btwnexchand  36044  linecgrand  36100  endofsegidand  36104  btwnconn1lem4  36108  btwnconn1lem8  36112  btwnconn1lem11  36115  btwnconn1lem12  36116  brsegle2  36127  seglecgr12im  36128  segleantisym  36133  colinbtwnle  36136  broutsideof2  36140  outsideoftr  36147  outsidele  36150  lineelsb2  36166  linethru  36171  gtinf  36337  weiunpo  36483  copsex2d  37157  relowlssretop  37381  pibt2  37435  heicant  37679  mbfresfi  37690  ftc1anclem6  37722  eqvreltrd  38626  riotasv2d  38975  lcvnbtwn2  39045  lcvnbtwn3  39046  lcvexchlem4  39055  omlfh1N  39276  atlen0  39328  atlatmstc  39337  cvratlem  39440  lnnat  39446  2atlt  39458  athgt  39475  1cvratex  39492  ps-2  39497  llncmp  39541  llncvrlpln  39577  lplncmp  39581  lplncvrlvol  39635  lvolcmp  39636  dalemcea  39679  dalem-cly  39690  dalem10  39692  dalem17  39699  dalem25  39717  dalem38  39729  dalem44  39735  dalem55  39746  2atm2atN  39804  cdlema1N  39810  paddasslem5  39843  dalawlem3  39892  dalawlem7  39896  dalawlem11  39900  dalawlem12  39901  lhp0lt  40022  4atexlemc  40088  cdlemg33a  40725  cdlemg33  40730  cdlemk51  40972  dia2dimlem2  41084  dia2dimlem3  41085  dihmeetlem20N  41345  coprmdvds2d  42014  flt4lem2  42670  flt4lem5f  42680  ismrcd2  42722  pellqrex  42902  jm2.17b  42985  jm2.26lem3  43025  fnwe2lem2  43075  omabs2  43356  addrcom  44499  infxrunb2  45395  0ellimcdiv  45678  dvnprodlem1  45975  stoweidlem15  46044  stoweidlem26  46055  stoweidlem28  46057  stoweidlem32  46061  stoweidlem44  46073  meadjuni  46486  natglobalincr  46906  dfatcolem  47284  icceuelpart  47450  perfectALTVlem1  47735  bgoldbtbndlem2  47820  bgoldbtbndlem3  47821  copisnmnd  48144  assintopass  48189  lcoss  48412  islindeps2  48459  isldepslvec2  48461  difmodm1lt  48502  isisod  48997  euendfunc  49411