Theorem adantrr 715

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 485	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan2 594	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  ad2antrl  726  ad2ant2r  745  ad2ant2lr  746  cases2ALT  1043  consensus  1047  3adant3  1128  3ad2antr1  1184  reusv2lem3  5301  axprlem4  5327  otsndisj  5409  otiunsndisj  5410  po2nr  5487  sotric  5501  sotrieq  5502  tz7.7  6217  fmptsnd  6931  fvtp1g  6960  f1cofveqaeqALT  7017  fsnex  7039  isocnv  7083  isores2  7086  isomin  7090  isoini  7091  f1oiso2  7105  ovmpodf  7306  offval  7416  ordsucun  7540  xp1st  7721  cnvf1olem  7805  fnse  7827  mpoxopoveq  7885  wfrlem3  7956  oalim  8157  omlim  8158  oaass  8187  omordi  8192  omwordri  8198  odi  8205  oen0  8212  oewordri  8218  nnawordi  8247  nnmordi  8257  omabs  8274  erinxp  8371  dom2lem  8549  mapen  8681  ssenen  8691  ssfi  8738  domfi  8739  domunfican  8791  mapfien  8871  ordtypelem6  8987  ordtypelem7  8988  card2inf  9019  inf3lem6  9096  cantnfle  9134  cantnflem1b  9149  cantnflem1  9152  wemapwe  9160  rankxplim3  9310  fseqenlem2  9451  dfac5lem4  9552  dfac2b  9556  cfsuc  9679  cfflb  9681  cofsmo  9691  infpssrlem4  9728  fin4en1  9731  ssfin4  9732  fin23lem26  9747  fin23lem22  9749  fin23lem27  9750  isf34lem4  9799  isf34lem5  9800  fin1a2lem12  9833  axdc3lem2  9873  axdc4lem  9877  ttukeylem6  9936  iundom2g  9962  pwcfsdom  10005  gchen2  10048  gchor  10049  fpwwe2lem7  10058  fpwwe2lem9  10060  fpwwe2lem11  10062  fpwwe2lem12  10063  fpwwe2  10065  pwfseqlem4  10084  gchina  10121  ltexprlem6  10463  prlem936  10469  mul4  10808  2addsub  10900  muladd  11072  ltleadd  11123  leord1  11167  eqord1  11168  ltord2  11169  leord2  11170  eqord2  11171  divmul3  11303  divcan7  11349  divadddiv  11355  lemul2a  11495  lemul12b  11497  ltmuldiv2  11514  ltdivmul  11515  ledivmul  11516  ltdivmul2  11517  lt2mul2div  11518  ledivmul2  11519  lemuldiv2  11521  lt2msq  11525  ltdiv23  11531  lediv23  11532  fimaxre  11584  supadd  11609  supmullem1  11611  cju  11634  zextlt  12057  suprzcl  12063  zmax  12346  xrlttr  12534  xrre3  12565  qbtwnre  12593  xrsupsslem  12701  xrinfmsslem  12702  supxrunb1  12713  supxrunb2  12714  ixxdisj  12754  iooshf  12816  icodisj  12863  iccf1o  12883  modid  13265  modadd1  13277  modmul1  13293  seqf1o  13412  expsub  13478  sqlecan  13572  bcval5  13679  hashmap  13797  hashfacen  13813  seqcoll  13823  swrdswrdlem  14066  swrdccatin2  14091  cshwidxmod  14165  2cshwcshw  14187  cshwcshid  14189  resqreu  14612  lenegsq  14680  limsupbnd2  14840  icco1  14897  rlimresb  14922  rlimsqzlem  15005  rlimsqz  15006  rlimsqz2  15007  caucvgrlem  15029  fsum0diag2  15138  o1fsum  15168  ruclem8  15590  dvdsmulcr  15639  ndvdsadd  15761  bitsshft  15824  lcmdvds  15952  hashdvds  16112  eulerthlem2  16119  phisum  16127  pcqmul  16190  pcmpt  16228  prmreclem3  16254  4sqlem11  16291  0ram  16356  ramub1  16364  invfun  17034  initoeu2lem2  17275  coaval  17328  catcisolem  17366  funcestrcsetclem8  17397  fullestrcsetc  17401  embedsetcestrclem  17407  funcsetcestrclem8  17412  fullsetcestrc  17416  prfcl  17453  prf1st  17454  prf2nd  17455  1st2ndprf  17456  curfuncf  17488  isposd  17565  lubun  17733  isacs3lem  17776  pslem  17816  psss  17824  pwsdiagmhm  17995  gsumccatOLD  18005  grpinvid1  18154  grpinvid2  18155  grplcan  18161  grpnpncan0  18195  dfgrp3lem  18197  dfgrp3  18198  grplactcnv  18202  0nsg  18321  eqger  18330  resghm  18374  conjghm  18389  subgga  18430  gaorber  18438  gastacl  18439  orbsta  18443  symgextf1lem  18548  psgnunilem2  18623  odid  18666  odmulg  18683  gexid  18706  odcau  18729  lsmssv  18768  lsmcom2  18780  pj1ghm  18829  frgpuptf  18896  frgpup1  18901  ghmplusg  18966  cyggex2  19017  gsumval3eu  19024  gsumval3  19027  ablfac1eu  19195  pgpfac1lem5  19201  ablsimpgfind  19232  isdrngd  19527  issrngd  19632  lmhmf1o  19818  lmhmima  19819  lmhmpreima  19820  lspextmo  19828  pwssplit2  19832  pwssplit3  19833  lspdisj  19897  islbs3  19927  lbsextlem4  19933  drngnidl  20002  lidldvgen  20028  issubassa2  20121  psrbagconf1o  20154  evlslem2  20292  mhplss  20342  ply1sclf1  20457  cnsubrg  20605  znunit  20710  cygznlem3  20716  dsmmsubg  20887  dsmmlss  20888  frlmsslsp  20940  frlmup1  20942  lindfrn  20965  f1lindf  20966  mamuass  21011  dmatmul  21106  dmatsubcl  21107  dmatmulcl  21109  dmatcrng  21111  scmataddcl  21125  scmatsubcl  21126  scmatcrng  21130  mdetunilem2  21222  pm2mpf1  21407  pm2mpghm  21424  eltg2  21566  ntrss  21663  opncldf1  21692  ssnei2  21724  neindisj  21725  restopnb  21783  restntr  21790  tgcmp  22009  hauscmplem  22014  2ndc1stc  22059  2ndcdisj  22064  2ndcomap  22066  restlly  22091  lly1stc  22104  isref  22117  islocfin  22125  comppfsc  22140  txcls  22212  txdis1cn  22243  pthaus  22246  txlm  22256  qtoptop2  22307  qtopomap  22326  kqt0lem  22344  pt1hmeo  22414  ptuncnv  22415  xkocnv  22422  fbasfip  22476  fgabs  22487  fbasrn  22492  elfm2  22556  fmfnfmlem2  22563  fmfnfmlem4  22565  ptcmplem3  22662  ptcmplem4  22663  tsmsres  22752  tsmsxplem1  22761  utoptop  22843  elbl2ps  22999  elbl2  23000  blin  23031  xmeter  23043  xmetresbl  23047  stdbdxmet  23125  metrest  23134  metustexhalf  23166  dscmet  23182  nrmmetd  23184  tngngp2  23261  nmoi2  23339  icccmplem2  23431  reconnlem2  23435  metdstri  23459  metdsle  23460  metdsre  23461  metnrmlem3  23469  fsumcn  23478  icccvx  23554  bndth  23562  evth  23563  reparphti  23601  pi1blem  23643  tcphcph  23840  iscfil2  23869  cfilfcls  23877  iscau4  23882  iscauf  23883  caucfil  23886  cncmet  23925  minveclem7  24038  ovoliunlem1  24103  ovolicc2lem2  24119  ovolicc2lem3  24120  ovolicc2lem4  24121  ovolicc2lem5  24122  ovolicc2  24123  voliunlem3  24153  voliun  24155  ioombl  24166  volivth  24208  ismbfd  24240  ismbf3d  24255  itg1addlem1  24293  i1fadd  24296  itg1addlem4  24300  itg2split  24350  itg2monolem1  24351  itg2gt0  24361  ibllem  24365  itgvallem3  24386  iblposlem  24392  dvmptfsum  24572  rolle  24587  dvlip  24590  c1liplem1  24593  lhop1  24611  lhop2  24612  dvcvx  24617  dvfsumge  24619  dvfsumrlimge0  24627  dvfsumrlim  24628  dvfsum2  24631  mdegaddle  24668  mdegvscale  24669  mdegmullem  24672  ply1divex  24730  coeeulem  24814  plyco  24831  dgrlt  24856  vieta1  24901  ulmss  24985  ulmdvlem3  24990  iblulm  24995  tanord  25122  eff1olem  25132  logdivlt  25204  logccv  25246  lawcos  25394  xrlimcnp  25546  cxp2limlem  25553  cxp2lim  25554  cxploglim2  25556  divsqrtsumo1  25561  lgambdd  25614  sqff1o  25759  dvdsppwf1o  25763  dvdsflf1o  25764  musum  25768  muinv  25770  fsumdvdsmul  25772  sgmmul  25777  fsumvma  25789  logfac2  25793  chpchtsum  25795  logfacrlim  25800  logexprlim  25801  dchrelbas3  25814  dchrmulcl  25825  bposlem1  25860  lgsdchr  25931  lgsquadlem1  25956  lgsquadlem2  25957  lgsquad2lem2  25961  chebbnd1lem1  26045  chpchtlim  26055  rplogsumlem2  26061  dchrmusum2  26070  dchrvmasumlem1  26071  dchrvmasum2lem  26072  dchrvmasumlem2  26074  dchrvmasumlem3  26075  dchrvmasumiflem2  26078  dchrisum0flb  26086  dchrisum0fno1  26087  rpvmasum2  26088  dchrisum0re  26089  dchrisum0lem1  26092  dchrisum0lem2a  26093  dchrisum0lem2  26094  dchrisum0lem3  26095  rplogsum  26103  mulogsum  26108  mulog2sumlem2  26111  vmalogdivsum2  26114  2vmadivsumlem  26116  selberglem2  26122  selberg3lem1  26133  selberg4lem1  26136  selberg4  26137  pntrsumo1  26141  selberg34r  26147  pntrlog2bndlem1  26153  pntrlog2bndlem2  26154  pntrlog2bndlem3  26155  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  pntrlog2bndlem6  26159  pntibndlem3  26168  pntlemp  26186  ostthlem1  26203  ostth3  26214  ercgrg  26303  oppperpex  26539  axlowdimlem15  26742  axlowdimlem16  26743  axcontlem10  26759  cusgrfilem1  27237  upgriswlk  27422  crctcshwlkn0  27599  wwlksnext  27671  wwlksnextwrd  27675  clwlkclwwlklem2a  27776  wwlksext2clwwlk  27836  grpoidinv  28285  grporcan  28295  grpoinvid1  28305  grpoinvid2  28306  grpolcan  28307  ablo4  28327  nvabs  28449  minvecolem7  28660  htthlem  28694  hvadd4  28813  hvaddsub4  28855  shscli  29094  pjspansn  29354  fh1  29395  fh2  29396  cm2j  29397  chscllem2  29415  spansncvi  29429  5oalem2  29432  5oalem5  29435  5oalem6  29436  3oalem2  29440  hoadd4  29561  cnvunop  29695  bralnfn  29725  eighmorth  29741  hmops  29797  hmopm  29798  adjlnop  29863  adjmul  29869  adjadd  29870  nmopcoi  29872  kbass5  29897  kbass6  29898  hstle  30007  stlesi  30018  mdsl0  30087  mdexchi  30112  atom1d  30130  superpos  30131  cvexchlem  30145  atomli  30159  atcvatlem  30162  chirredlem2  30168  chirredlem3  30169  atcvat4i  30174  mdsymlem1  30180  mdsymlem3  30182  mdsymlem5  30184  mdsymlem6  30185  sumdmdlem  30195  sumdmdlem2  30196  cdj1i  30210  opeldifid  30349  isoun  30437  1stpreimas  30441  f1od2  30457  ccatf1  30625  archirngz  30818  archiabllem1  30822  archiabllem2c  30824  rngurd  30857  qusxpid  30928  indf1ofs  31285  esum2d  31352  cntmeas  31485  ddemeas  31495  carsgclctunlem1  31575  itgeq12dv  31584  eulerpartlemgc  31620  eulerpartlemb  31626  eulerpartlemgs2  31638  ballotlemfc0  31750  ballotlemfcc  31751  reprss  31888  reprpmtf1o  31897  hgt750lemb  31927  bnj607  32188  derangenlem  32418  subfacp1lem3  32429  subfacp1lem5  32431  cvmliftmolem2  32529  cvmliftlem6  32537  cvmlift2lem5  32554  cvmlift2lem7  32556  cvmlift2lem9  32558  mppspstlem  32818  dfon2lem6  33033  frrlem3  33125  frrlem13  33135  sltres  33169  noresle  33200  nosupno  33203  colinbtwnle  33579  finminlem  33666  nn0prpwlem  33670  isfne  33687  neibastop1  33707  neibastop2lem  33708  neibastop3  33710  tailfb  33725  onsuct0  33789  nndivsub  33805  knoppcnlem6  33837  knoppndvlem9  33859  knoppndvlem18  33868  knoppndvlem21  33871  bj-prmoore  34410  bj-finsumval0  34570  rdgeqoa  34654  pibt2  34701  lindsadd  34900  matunitlindflem2  34904  poimirlem4  34911  poimirlem11  34918  poimirlem12  34919  poimirlem13  34920  poimirlem25  34932  poimirlem28  34935  heicant  34942  mblfinlem2  34945  mblfinlem3  34946  mblfinlem4  34947  mbfposadd  34954  itg2addnclem3  34960  bddiblnc  34977  ftc1anclem5  34986  ftc1anclem6  34987  ftc1anclem7  34988  ftc1anc  34990  frinfm  35025  filbcmb  35030  seqpo  35037  sstotbnd2  35067  isbndx  35075  ssbnd  35081  prdsbnd  35086  ismtycnv  35095  ismtyres  35101  heiborlem3  35106  heibor  35114  ghomdiv  35185  grpokerinj  35186  isdrngo2  35251  rngohomco  35267  rngoisocnv  35274  rngoisoco  35275  crngm4  35296  crngohomfo  35299  isidlc  35308  ispridl2  35331  ispridlc  35363  prtlem16  36020  ax12eq  36092  ax12el  36093  lshpcmp  36139  omllaw3  36396  omlfh1N  36409  cvratlem  36572  cvrat3  36593  cvrat4  36594  ps-2  36629  elpaddn0  36951  paddasslem10  36980  cdleme0cp  37365  cdleme32a  37592  cdlemeg49lebilem  37690  cdleme50eq  37692  tendoeq2  37925  diaglbN  38206  diameetN  38207  diainN  38208  dvhopN  38267  djaclN  38287  djajN  38288  dihopelvalcpre  38399  dih1dimatlem  38480  dihmeetcl  38496  djhcl  38551  mapdpglem2  38824  frlmsnic  39198  0prjspn  39319  ismrc  39347  eldioph2  39408  lzenom  39416  rexrabdioph  39440  fphpdo  39463  irrapxlem3  39470  elpell14qr2  39508  pell14qrreccl  39510  pell14qrdich  39515  pellfundglb  39531  monotoddzzfi  39588  2nn0ind  39591  jm2.21  39640  jm2.22  39641  dnnumch3  39696  dnwech  39697  fnwe2lem2  39700  hbtlem6  39778  imo72b2lem1  40570  mnuprdlem1  40657  mnuprdlem2  40658  cncmpmax  41338  disjf1  41492  eliccelioc  41846  fprodexp  41924  fprodabs2  41925  mullimc  41946  mullimcf  41953  islpcn  41969  limsuppnfdlem  42031  liminfval2  42098  xlimmnfvlem1  42162  xlimmnfvlem2  42163  xlimpnfvlem1  42166  xlimpnfvlem2  42167  cncfshift  42206  cncfperiod  42211  fprodcncf  42233  dvnprodlem1  42280  dvnprodlem2  42281  stoweidlem34  42368  stoweidlem48  42382  stoweidlem60  42394  fourierdlem42  42483  fourierdlem60  42500  fourierdlem61  42501  fourierdlem63  42503  fourierdlem65  42505  fourierdlem87  42527  fourierdlem97  42537  elaa2  42568  etransclem46  42614  etransc  42617  sge0iunmptlemfi  42744  isomennd  42862  ovnsslelem  42891  ovolval4lem2  42981  ovolval5lem3  42985  smflimlem3  43098  smflimlem4  43099  smflimlem6  43101  smfpimbor1lem1  43122  smflimmpt  43133  smflimsupmpt  43152  smfliminfmpt  43155  fvelsetpreimafv  43596  icceuelpart  43645  prproropf1olem4  43717  fmtnoprmfac2  43778  bgoldbtbndlem2  44020  bgoldbtbndlem3  44021  srhmsubc  44396  srhmsubcALTV  44414  aacllem  44951