Theorem mp2and 698

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 694	. 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  3758  ssnelpssd  4138  frpomin  6372  fvf1pr  7343  tfisi  7896  tfindsg2  7899  mposn  8144  frxp2  8185  smoord  8421  oelimcl  8656  oeeui  8658  nnawordex  8693  omabs  8707  naddssim  8741  naddel12  8756  ertrd  8779  en2prd  9114  omxpenlem  9139  fodomfir  9396  ixpfi2  9420  oismo  9609  cantnflem1c  9756  cantnflem1  9758  cantnflem3  9760  infxpenc2  10091  isfin2-2  10388  axdc2lem  10517  r1limwun  10805  letrd  11447  lelttrd  11448  ltletrd  11450  lttrd  11451  le2addd  11909  le2subd  11910  ltleaddd  11911  leltaddd  11912  lt2subd  11914  ltmul12a  12150  lemul12ad  12237  lemul12bd  12238  lt2halvesd  12541  uzind  12735  uztrn  12921  xrlttrd  13221  xrlelttrd  13222  xrltletrd  13223  xrletrd  13224  supxrunb1  13381  supxrunb2  13382  ixxun  13423  ixxss1  13425  ixxss2  13426  ixxss12  13427  fldiv4p1lem1div2  13886  fldiv4lem1div2uz2  13887  seqf1o  14094  faclbnd3  14341  relexpindlem  15112  01sqrexlem1  15291  01sqrexlem4  15294  01sqrexlem7  15297  abs3lemd  15510  rlimcn3  15636  o1of2  15659  lo1add  15673  lo1mul  15674  modfsummod  15842  mertenslem1  15932  sin01gt0  16238  cos01gt0  16239  sin02gt0  16240  dvds2addd  16340  dvds2subd  16341  dvdstrd  16343  bezoutlem4  16589  mulgcd  16595  lcmgcdeq  16659  mulgcddvds  16702  rpmulgcd2  16703  rpdvds  16707  divgcdcoprmex  16713  phimullem  16826  eulerthlem1  16828  eulerthlem2  16829  prmdiveq  16833  pythagtriplem4  16866  pcqmul  16900  pcgcd1  16924  pcadd  16936  pockthlem  16952  prmreclem2  16964  4sqlem16  17007  ramub1lem1  17073  ramub1lem2  17074  prmgaplem7  17104  iscatd2  17739  cicsym  17865  initoeu2  18083  joinval  18447  meetval  18461  lattrd  18516  latledi  18547  mulgass  19151  gaorber  19348  psgnunilem4  19539  efgredlem  19789  odadd2  19891  dmdprdpr  20093  ablfacrp2  20111  ablfac1b  20114  ablfac1eu  20117  pgpfac1  20124  gsumbagdiaglem  21973  mdetunilem1  22639  mdetunilem4  22642  mdetunilem9  22647  neiptoptop  23160  lmcnp  23333  txcls  23633  txlly  23665  txnlly  23666  tx1stc  23679  alexsubALTlem1  24076  prdsmet  24401  blin2  24460  blcvx  24839  tgqioo  24841  metnrmlem3  24902  iscmet3lem2  25345  ovolmge0  25531  ovolunlem2  25552  mbfi1flimlem  25777  mbfmullem  25780  itg2add  25814  dvferm1lem  26042  dvferm2lem  26044  dvlip2  26054  dvge0  26065  dvcvx  26079  dvfsumabs  26083  ftc1a  26098  plyadd  26276  plymul  26277  dgrlb  26295  plydivlem4  26356  vieta1lem2  26371  ulmdvlem3  26463  sinq12gt0  26567  logdivlti  26680  fsumharmonic  27073  mpodvdsmulf1o  27255  dvdsmulf1o  27257  logfacubnd  27283  perfectlem1  27291  dchrptlem2  27327  2sqlem5  27484  2sqlem8  27488  2sqmod  27498  dchrisum0flblem2  27571  pntibndlem2  27653  pntlemr  27664  pntlemp  27672  nosupbnd1  27777  nosupbnd2lem1  27778  nosupbnd2  27779  noinfbnd1  27792  noinfbnd2lem1  27793  noinfbnd2  27794  noetasuplem4  27799  noetainflem4  27803  slttrd  27822  sltletrd  27823  slelttrd  27824  sletrd  27825  oldbdayim  27945  mulsproplem5  28164  mulsproplem6  28165  mulsproplem7  28166  mulsproplem8  28167  sltmuld  28181  axtgpasch  28493  tgjustr  28500  wlkcompim  29668  wwlksnredwwlkn  29928  wwlksnextsurj  29933  upgr4cycl4dv4e  30217  ex-natded5.2-2  30437  chscllem2  31670  chscllem4  31672  nmopge0  31943  nmfnge0  31959  nmoptrii  32126  staddi  32278  stadd3i  32280  atcvatlem  32417  supssd  32723  infssd  32724  xrofsup  32774  xrge0addgt0  33003  archiabllem2c  33175  orngmul  33298  linds2eq  33374  ssdifidlprm  33451  lbsdiflsp0  33639  fedgmullem2  33643  esumpmono  34043  unelldsys  34122  omssubaddlem  34264  signstfvneq0  34549  axtgupdim2ALTV  34645  bnj1098  34759  bnj1110  34958  bnj1121  34961  0nn0m1nnn0  35080  cplgredgex  35088  erdszelem8  35166  txsconn  35209  cvmlift2lem10  35280  cvmlift3lem7  35293  sotrd  35727  dfon2lem6  35752  dfon2lem8  35754  cgrtr4d  35949  cgrtrand  35957  cgrtr3and  35959  cgrextendand  35973  btwnexch3and  35985  btwnexchand  35990  linecgrand  36046  endofsegidand  36050  btwnconn1lem4  36054  btwnconn1lem8  36058  btwnconn1lem11  36061  btwnconn1lem12  36062  brsegle2  36073  seglecgr12im  36074  segleantisym  36079  colinbtwnle  36082  broutsideof2  36086  outsideoftr  36093  outsidele  36096  lineelsb2  36112  linethru  36117  gtinf  36285  weiunpo  36431  copsex2d  37105  relowlssretop  37329  pibt2  37383  heicant  37615  mbfresfi  37626  ftc1anclem6  37658  eqvreltrd  38564  riotasv2d  38913  lcvnbtwn2  38983  lcvnbtwn3  38984  lcvexchlem4  38993  omlfh1N  39214  atlen0  39266  atlatmstc  39275  cvratlem  39378  lnnat  39384  2atlt  39396  athgt  39413  1cvratex  39430  ps-2  39435  llncmp  39479  llncvrlpln  39515  lplncmp  39519  lplncvrlvol  39573  lvolcmp  39574  dalemcea  39617  dalem-cly  39628  dalem10  39630  dalem17  39637  dalem25  39655  dalem38  39667  dalem44  39673  dalem55  39684  2atm2atN  39742  cdlema1N  39748  paddasslem5  39781  dalawlem3  39830  dalawlem7  39834  dalawlem11  39838  dalawlem12  39839  lhp0lt  39960  4atexlemc  40026  cdlemg33a  40663  cdlemg33  40668  cdlemk51  40910  dia2dimlem2  41022  dia2dimlem3  41023  dihmeetlem20N  41283  coprmdvds2d  41958  flt4lem2  42602  flt4lem5f  42612  ismrcd2  42655  pellqrex  42835  jm2.17b  42918  jm2.26lem3  42958  fnwe2lem2  43008  omabs2  43294  addrcom  44444  infxrunb2  45283  0ellimcdiv  45570  stoweidlem15  45936  stoweidlem26  45947  stoweidlem28  45949  stoweidlem32  45953  stoweidlem44  45965  meadjuni  46378  natglobalincr  46796  dfatcolem  47170  icceuelpart  47310  perfectALTVlem1  47595  bgoldbtbndlem2  47680  bgoldbtbndlem3  47681  copisnmnd  47892  assintopass  47937  lcoss  48165  islindeps2  48212  isldepslvec2  48214  difmodm1lt  48256