Theorem adantrr 729

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypothesis

Ref	Expression
adant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
adantrr	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝜒)

Proof of Theorem adantrr

Step	Hyp	Ref	Expression
1		simpl 487	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan2 604	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ad2antrl  740  ad2ant2r  759  ad2ant2lr  760  cases2ALT  1064  consensus  1068  3adant3  1150  3ad2antr1  1207  reusv2lem3  5373  axprlem4OLD  5403  otsndisj  5504  otiunsndisj  5505  po2nr  5585  sotric  5601  sotrieq  5602  tz7.7  6388  fmptsnd  7169  fvtp1g  7198  f1cofveqaeqALT  7258  fsnex  7283  isocnv  7330  isores2  7333  isomin  7337  isoini  7338  f1oiso2  7352  ovmpodf  7568  offval  7685  ordsucun  7822  xp1st  8019  cnvf1olem  8106  fnse  8130  sexp2  8143  mpoxopoveq  8216  frrlem3  8286  frrlem13  8296  oalim  8518  omlim  8519  oaass  8547  omordi  8552  omwordri  8558  odi  8565  oen0  8573  oewordri  8579  nnawordi  8608  nnmordi  8618  omabs  8638  coflton  8658  nadd4  8686  erinxp  8790  dom2lem  8990  domssl  8996  mapen  9130  ssenen  9140  ssfiALT  9159  domfi  9174  php  9192  domunfican  9282  mapfien  9369  ordtypelem6  9486  ordtypelem7  9487  card2inf  9518  inf3lem6  9603  cantnfle  9641  cantnflem1b  9656  cantnflem1  9659  wemapwe  9667  ttrclselem2  9696  rankxplim3  9854  fseqenlem2  10010  dfac5lem4  10111  dfac2b  10115  cfsuc  10242  cfflb  10244  cofsmo  10254  infpssrlem4  10291  fin4en1  10294  ssfin4  10295  fin23lem26  10310  fin23lem22  10312  fin23lem27  10313  isf34lem4  10362  isf34lem5  10363  fin1a2lem12  10396  axdc3lem2  10436  axdc4lem  10440  ttukeylem6  10499  iundom2g  10525  pwcfsdom  10569  gchen2  10612  gchor  10613  fpwwe2lem6  10622  fpwwe2lem8  10624  fpwwe2lem10  10626  fpwwe2lem11  10627  fpwwe2  10629  pwfseqlem4  10648  gchina  10685  ltexprlem6  11027  prlem936  11033  mul4  11379  2addsub  11472  muladd  11647  ltleadd  11698  leord1  11742  eqord1  11743  ltord2  11744  leord2  11745  eqord2  11746  divmul3  11878  divcan7  11925  divadddiv  11931  lemul2a  12071  lemul12b  12073  ltmuldiv2  12090  ltdivmul  12091  ledivmul  12092  ltdivmul2  12093  lt2mul2div  12094  ledivmul2  12095  lemuldiv2  12097  lt2msq  12101  ltdiv23  12107  lediv23  12108  fimaxre  12160  supadd  12184  supmullem1  12186  cju  12215  zextlt  12671  suprzcl  12677  zmax  12970  xrlttr  13166  xrre3  13198  qbtwnre  13226  xrsupsslem  13334  xrinfmsslem  13335  supxrunb1  13346  supxrunb2  13347  ixxdisj  13388  iooshf  13454  icodisj  13504  iccf1o  13524  modid  13931  modadd1  13943  modmul1  13962  seqf1o  14081  expsub  14148  sqlecan  14247  bcval5  14356  hashmap  14474  hashfacen  14493  seqcoll  14503  swrdswrdlem  14743  swrdccatin2  14768  cshwidxmod  14842  2cshwcshw  14864  cshwcshid  14866  resqreu  15305  lenegsq  15374  limsupbnd2  15536  icco1  15593  rlimresb  15618  rlimsqzlem  15702  rlimsqz  15703  rlimsqz2  15704  caucvgrlem  15726  fsum0diag2  15836  o1fsum  15867  ruclem8  16294  dvdsmulcr  16344  ndvdsadd  16469  bitsshft  16534  lcmdvds  16667  hashdvds  16835  eulerthlem2  16842  phisum  16851  pcqmul  16914  pcmpt  16953  prmreclem3  16979  4sqlem11  17016  0ram  17081  ramub1  17089  invfun  17822  initoeu2lem2  18073  coaval  18126  catcisolem  18168  funcestrcsetclem8  18204  fullestrcsetc  18208  embedsetcestrclem  18214  funcsetcestrclem8  18219  fullsetcestrc  18223  prfcl  18260  prf1st  18261  prf2nd  18262  1st2ndprf  18263  curfuncf  18295  isposd  18379  lubun  18572  isacs3lem  18599  pslem  18629  psss  18637  chnccat  18683  chnpof1  18687  pwsdiagmhm  18891  grpinvid1  19059  grpinvid2  19060  grplcan  19068  grpnpncan0  19103  dfgrp3lem  19105  dfgrp3  19106  grplactcnv  19110  0nsg  19236  eqger  19247  qusxpid  19252  eqg0subg  19268  qus0subgadd  19271  resghm  19303  conjghm  19320  subgga  19371  gaorber  19379  gastacl  19380  orbsta  19384  symgextf1lem  19491  psgnunilem2  19566  odid  19609  odmulg  19627  gexid  19652  odcau  19675  lsmssv  19714  lsmcom2  19726  pj1ghm  19774  frgpuptf  19841  frgpup1  19846  ghmplusg  19917  cyggex2  19968  gsumval3eu  19975  gsumval3  19978  ablfac1eu  20146  pgpfac1lem5  20152  ablsimpgfind  20183  ringurd  20268  srhmsubc  20766  isdomn4  20801  isdrngd  20850  isdrngdOLD  20852  issrngd  20939  lmhmf1o  21148  lmhmima  21149  lmhmpreima  21150  lspextmo  21158  pwssplit2  21162  pwssplit3  21163  lspdisj  21230  islbs3  21260  lbsextlem4  21266  drngnidl  21358  rngqiprngghmlem2  21409  rngqiprnglinlem1  21412  rngqiprngghm  21420  lidldvgen  21483  cnsubrg  21558  znunit  21694  cygznlem3  21700  dsmmsubg  21874  dsmmlss  21875  frlmsslsp  21927  frlmup1  21929  lindfrn  21952  f1lindf  21953  issubassa2  22023  psrbagconf1o  22060  psrgrp  22087  evlslem2  22211  mhplss  22299  psdmul  22310  psdmvr  22313  ply1sclf1  22431  mamuass  22540  dmatmul  22635  dmatsubcl  22636  dmatmulcl  22638  dmatcrng  22640  scmataddcl  22654  scmatsubcl  22655  scmatcrng  22659  mdetunilem2  22751  pm2mpf1  22937  pm2mpghm  22954  eltg2  23096  ntrss  23193  opncldf1  23222  ssnei2  23254  neindisj  23255  restopnb  23313  restntr  23320  tgcmp  23539  hauscmplem  23544  2ndc1stc  23589  2ndcdisj  23594  2ndcomap  23596  restlly  23621  lly1stc  23634  isref  23647  islocfin  23655  comppfsc  23670  txcls  23742  txdis1cn  23773  pthaus  23776  txlm  23786  qtoptop2  23837  qtopomap  23856  kqt0lem  23874  pt1hmeo  23944  ptuncnv  23945  xkocnv  23952  fbasfip  24006  fgabs  24017  fbasrn  24022  elfm2  24086  fmfnfmlem2  24093  fmfnfmlem4  24095  ptcmplem3  24192  ptcmplem4  24193  tsmsres  24282  tsmsxplem1  24291  utoptop  24372  elbl2ps  24527  elbl2  24528  blin  24559  xmeter  24571  xmetresbl  24575  stdbdxmet  24653  metrest  24662  metustexhalf  24694  dscmet  24710  nrmmetd  24712  tngngp2  24790  nmoi2  24868  icccmplem2  24962  reconnlem2  24966  metdstri  24990  metdsle  24991  metdsre  24992  metnrmlem3  25000  fsumcn  25010  icccvx  25090  bndth  25098  evth  25099  reparphti  25137  pi1blem  25179  tcphcph  25377  iscfil2  25406  cfilfcls  25414  iscau4  25419  iscauf  25420  caucfil  25423  cncmet  25462  minveclem7  25575  ovoliunlem1  25642  ovolicc2lem2  25658  ovolicc2lem3  25659  ovolicc2lem4  25660  ovolicc2lem5  25661  ovolicc2  25662  voliunlem3  25692  voliun  25694  ioombl  25705  volivth  25747  ismbfd  25779  ismbf3d  25794  itg1addlem1  25832  i1fadd  25835  itg1addlem4  25839  itg2split  25889  itg2monolem1  25890  itg2gt0  25900  ibllem  25904  itgvallem3  25926  iblposlem  25932  bddiblnc  25982  dvmptfsum  26115  rolle  26130  dvlip  26133  c1liplem1  26136  lhop1  26154  lhop2  26155  dvcvx  26160  dvfsumge  26162  dvfsumrlimge0  26170  dvfsumrlim  26171  dvfsum2  26174  mdegaddle  26212  mdegvscale  26213  mdegmullem  26216  ply1divex  26275  coeeulem  26362  plyco  26379  dgrlt  26404  vieta1  26454  ulmss  26541  ulmdvlem3  26546  iblulm  26551  tanord  26684  eff1olem  26694  logdivlt  26767  logccv  26809  lawcos  26962  xrlimcnp  27114  cxp2limlem  27121  cxp2lim  27122  cxploglim2  27124  divsqrtsumo1  27129  lgambdd  27182  sqff1o  27327  dvdsppwf1o  27331  dvdsflf1o  27332  musum  27336  muinv  27338  fsumdvdsmul  27340  sgmmul  27346  fsumvma  27358  logfac2  27362  chpchtsum  27364  logfacrlim  27369  logexprlim  27370  dchrelbas3  27383  dchrmulcl  27394  bposlem1  27429  lgsdchr  27500  lgsquadlem1  27525  lgsquadlem2  27526  lgsquad2lem2  27530  chebbnd1lem1  27614  chpchtlim  27624  rplogsumlem2  27630  dchrmusum2  27639  dchrvmasumlem1  27640  dchrvmasum2lem  27641  dchrvmasumlem2  27643  dchrvmasumlem3  27644  dchrvmasumiflem2  27647  dchrisum0flb  27655  dchrisum0fno1  27656  rpvmasum2  27657  dchrisum0re  27658  dchrisum0lem1  27661  dchrisum0lem2a  27662  dchrisum0lem2  27663  dchrisum0lem3  27664  rplogsum  27672  mulogsum  27677  mulog2sumlem2  27680  vmalogdivsum2  27683  2vmadivsumlem  27685  selberglem2  27691  selberg3lem1  27702  selberg4lem1  27705  selberg4  27706  pntrsumo1  27710  selberg34r  27716  pntrlog2bndlem1  27722  pntrlog2bndlem2  27723  pntrlog2bndlem3  27724  pntrlog2bndlem4  27725  pntrlog2bndlem5  27726  pntrlog2bndlem6  27728  pntibndlem3  27737  pntlemp  27755  ostthlem1  27772  ostth3  27783  ltsres  27807  noresle  27842  nosupno  27848  nosupbday  27850  noinfno  27863  bday1  27988  cutlt  28106  addsproplem2  28144  negsproplem2  28203  mulsuniflem  28323  mulsunif2lem  28343  precsexlem9  28389  precsexlem10  28390  precsexlem11  28391  om2noseqlt  28473  om2noseqlt2  28474  om2noseqf1o  28475  om2noseqrdg  28478  noseqrdgfn  28480  bdaypw2n0bndlem  28637  bdayfinbndlem1  28641  recut  28668  elreno2  28669  renegscl  28672  ercgrg  28767  oppperpex  29015  axlowdimlem15  29287  axlowdimlem16  29288  axcontlem10  29304  cusgrfilem1  29786  upgriswlk  29971  crctcshwlkn0  30151  wwlksnext  30223  wwlksnextwrd  30227  clwlkclwwlklem2a  30330  wwlksext2clwwlk  30389  grpoidinv  30841  grporcan  30851  grpoinvid1  30861  grpoinvid2  30862  grpolcan  30863  ablo4  30883  nvabs  31005  minvecolem7  31216  htthlem  31250  hvadd4  31369  hvaddsub4  31411  shscli  31650  pjspansn  31910  fh1  31951  fh2  31952  cm2j  31953  chscllem2  31971  spansncvi  31985  5oalem2  31988  5oalem5  31991  5oalem6  31992  3oalem2  31996  hoadd4  32117  cnvunop  32251  bralnfn  32281  eighmorth  32297  hmops  32353  hmopm  32354  adjlnop  32419  adjmul  32425  adjadd  32426  nmopcoi  32428  kbass5  32453  kbass6  32454  hstle  32563  stlesi  32574  mdsl0  32643  mdexchi  32668  atom1d  32686  superpos  32687  cvexchlem  32701  atomli  32715  atcvatlem  32718  chirredlem2  32724  chirredlem3  32725  atcvat4i  32730  mdsymlem1  32736  mdsymlem3  32738  mdsymlem5  32740  mdsymlem6  32741  sumdmdlem  32751  sumdmdlem2  32752  cdj1i  32766  opeldifid  32925  isoun  33028  1stpreimas  33032  f1od2  33045  indf1ofs  33167  ccatf1  33250  archirngz  33490  archiabllem1  33494  archiabllem2c  33496  esum2d  34464  cntmeas  34597  ddemeas  34607  carsgclctunlem1  34688  itgeq12dv  34697  eulerpartlemgc  34733  eulerpartlemb  34739  eulerpartlemgs2  34751  ballotlemfc0  34864  ballotlemfcc  34865  reprss  34985  reprpmtf1o  34994  hgt750lemb  35024  bnj607  35285  fissorduni  35461  derangenlem  35644  subfacp1lem3  35655  subfacp1lem5  35657  cvmliftmolem2  35755  cvmliftlem6  35763  cvmlift2lem5  35780  cvmlift2lem7  35782  cvmlift2lem9  35784  mppspstlem  36044  dfon2lem6  36259  colinbtwnle  36591  ltnadd  36676  nmulrid  36678  finminlem  36810  nn0prpwlem  36814  isfne  36831  neibastop1  36851  neibastop2lem  36852  neibastop3  36854  tailfb  36869  onsuct0  36933  nndivsub  36949  mh-inf3f1  37033  knoppcnlem6  37068  knoppndvlem9  37090  knoppndvlem18  37099  knoppndvlem21  37102  bj-prmoore  37738  bj-finsumval0  37910  rdgeqoa  37997  pibt2  38044  lindsadd  38245  matunitlindflem2  38249  poimirlem4  38256  poimirlem11  38263  poimirlem12  38264  poimirlem13  38265  poimirlem25  38277  poimirlem28  38280  heicant  38287  mblfinlem2  38290  mblfinlem3  38291  mblfinlem4  38292  mbfposadd  38299  itg2addnclem3  38305  ftc1anclem5  38329  ftc1anclem6  38330  ftc1anclem7  38331  ftc1anc  38333  frinfm  38367  filbcmb  38372  seqpo  38379  sstotbnd2  38406  isbndx  38414  ssbnd  38420  prdsbnd  38425  ismtycnv  38434  ismtyres  38440  heiborlem3  38445  heibor  38453  ghomdiv  38524  grpokerinj  38525  isdrngo2  38590  rngohomco  38606  rngoisocnv  38613  rngoisoco  38614  crngm4  38635  crngohomfo  38638  isidlc  38647  ispridl2  38670  ispridlc  38702  prtlem16  39624  ax12eq  39696  ax12el  39697  lshpcmp  39743  omllaw3  40000  omlfh1N  40013  cvratlem  40176  cvrat3  40197  cvrat4  40198  ps-2  40233  elpaddn0  40555  paddasslem10  40584  cdleme0cp  40969  cdleme32a  41196  cdlemeg49lebilem  41294  cdleme50eq  41296  tendoeq2  41529  diaglbN  41810  diameetN  41811  diainN  41812  dvhopN  41871  djaclN  41891  djajN  41892  dihopelvalcpre  42003  dih1dimatlem  42084  dihmeetcl  42100  djhcl  42155  mapdpglem2  42428  3factsumint1  42769  sticksstones22  42916  unitscyglem4  42946  imacrhmcl  43269  frlmsnic  43291  psrmnd  43294  evlselvlem  43303  fsuppind  43305  0prjspn  43343  infdesc  43358  ismrc  43415  eldioph2  43476  lzenom  43484  rexrabdioph  43504  fphpdo  43527  irrapxlem3  43534  elpell14qr2  43572  pell14qrreccl  43574  pell14qrdich  43579  pellfundglb  43595  monotoddzzfi  43652  2nn0ind  43655  jm2.21  43704  jm2.22  43705  dnnumch3  43757  dnwech  43758  fnwe2lem2  43761  hbtlem6  43839  cantnfresb  44034  imo72b2lem1  44878  mnuprdlem1  44965  mnuprdlem2  44966  relpmin  45644  traxext  45669  cncmpmax  45735  disjf1  45884  eliccelioc  46220  fprodexp  46293  fprodabs2  46294  mullimc  46315  mullimcf  46322  islpcn  46336  limsuppnfdlem  46398  liminfval2  46465  xlimmnfvlem1  46529  xlimmnfvlem2  46530  xlimpnfvlem1  46533  xlimpnfvlem2  46534  cncfshift  46571  cncfperiod  46576  fprodcncf  46597  dvnprodlem1  46643  dvnprodlem2  46644  stoweidlem34  46731  stoweidlem48  46745  stoweidlem60  46757  fourierdlem42  46846  fourierdlem60  46863  fourierdlem61  46864  fourierdlem63  46866  fourierdlem65  46868  fourierdlem87  46890  fourierdlem97  46900  elaa2  46931  etransclem46  46977  etransc  46980  salrestss  47058  sge0iunmptlemfi  47110  isomennd  47228  ovnsslelem  47257  ovolval4lem2  47347  smflimlem3  47470  smflimlem4  47471  smflimlem6  47473  smfpimbor1lem1  47495  smflimmpt  47507  smflimsupmpt  47526  smfliminfmpt  47529  fsetsnf1  47772  fcoresf1  47789  fvelsetpreimafv  48119  icceuelpart  48168  prproropf1olem4  48238  fmtnoprmfac2  48302  bgoldbtbndlem2  48554  bgoldbtbndlem3  48555  gpgnbgrvtx0  48822  gpgnbgrvtx1  48823  gpg3nbgrvtx0ALT  48825  gpg3nbgrvtx1  48826  srhmsubcALTV  49073  xpco2  49618  catprs  49772  uppropd  49942  thincciso2  50216  prsthinc  50225  functermc  50269  fulltermc  50272  lmdran  50432  cmdlan  50433  aacllem  50584