Theorem adantrr 717

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 482	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan2 593	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:  ad2antrl  728  ad2ant2r  747  ad2ant2lr  748  cases2ALT  1048  consensus  1052  3adant3  1132  3ad2antr1  1189  reusv2lem3  5375  axprlem4OLD  5404  otsndisj  5499  otiunsndisj  5500  po2nr  5580  sotric  5596  sotrieq  5597  tz7.7  6383  fmptsnd  7166  fvtp1g  7195  f1cofveqaeqALT  7256  fsnex  7281  isocnv  7328  isores2  7331  isomin  7335  isoini  7336  f1oiso2  7350  ovmpodf  7568  offval  7685  ordsucun  7824  xp1st  8025  cnvf1olem  8114  fnse  8137  sexp2  8150  mpoxopoveq  8223  frrlem3  8292  frrlem13  8302  wfrlem3OLD  8329  oalim  8549  omlim  8550  oaass  8578  omordi  8583  omwordri  8589  odi  8596  oen0  8603  oewordri  8609  nnawordi  8638  nnmordi  8648  omabs  8668  coflton  8688  nadd4  8715  erinxp  8810  dom2lem  9011  domssl  9017  mapen  9160  ssenen  9170  ssfiALT  9193  domfi  9208  php  9226  domunfican  9338  mapfien  9425  ordtypelem6  9542  ordtypelem7  9543  card2inf  9574  inf3lem6  9652  cantnfle  9690  cantnflem1b  9705  cantnflem1  9708  wemapwe  9716  ttrclselem2  9745  rankxplim3  9900  fseqenlem2  10044  dfac5lem4  10145  dfac5lem4OLD  10147  dfac2b  10150  cfsuc  10276  cfflb  10278  cofsmo  10288  infpssrlem4  10325  fin4en1  10328  ssfin4  10329  fin23lem26  10344  fin23lem22  10346  fin23lem27  10347  isf34lem4  10396  isf34lem5  10397  fin1a2lem12  10430  axdc3lem2  10470  axdc4lem  10474  ttukeylem6  10533  iundom2g  10559  pwcfsdom  10602  gchen2  10645  gchor  10646  fpwwe2lem6  10655  fpwwe2lem8  10657  fpwwe2lem10  10659  fpwwe2lem11  10660  fpwwe2  10662  pwfseqlem4  10681  gchina  10718  ltexprlem6  11060  prlem936  11066  mul4  11408  2addsub  11501  muladd  11674  ltleadd  11725  leord1  11769  eqord1  11770  ltord2  11771  leord2  11772  eqord2  11773  divmul3  11906  divcan7  11955  divadddiv  11961  lemul2a  12101  lemul12b  12103  ltmuldiv2  12121  ltdivmul  12122  ledivmul  12123  ltdivmul2  12124  lt2mul2div  12125  ledivmul2  12126  lemuldiv2  12128  lt2msq  12132  ltdiv23  12138  lediv23  12139  fimaxre  12191  supadd  12215  supmullem1  12217  cju  12241  zextlt  12672  suprzcl  12678  zmax  12966  xrlttr  13161  xrre3  13192  qbtwnre  13220  xrsupsslem  13328  xrinfmsslem  13329  supxrunb1  13340  supxrunb2  13341  ixxdisj  13382  iooshf  13448  icodisj  13498  iccf1o  13518  modid  13918  modadd1  13930  modmul1  13947  seqf1o  14066  expsub  14133  sqlecan  14232  bcval5  14341  hashmap  14458  hashfacen  14477  seqcoll  14487  swrdswrdlem  14727  swrdccatin2  14752  cshwidxmod  14826  2cshwcshw  14849  cshwcshid  14851  resqreu  15276  lenegsq  15344  limsupbnd2  15504  icco1  15561  rlimresb  15586  rlimsqzlem  15670  rlimsqz  15671  rlimsqz2  15672  caucvgrlem  15694  fsum0diag2  15804  o1fsum  15834  ruclem8  16260  dvdsmulcr  16310  ndvdsadd  16434  bitsshft  16499  lcmdvds  16632  hashdvds  16799  eulerthlem2  16806  phisum  16815  pcqmul  16878  pcmpt  16917  prmreclem3  16943  4sqlem11  16980  0ram  17045  ramub1  17053  invfun  17782  initoeu2lem2  18033  coaval  18086  catcisolem  18128  funcestrcsetclem8  18164  fullestrcsetc  18168  embedsetcestrclem  18174  funcsetcestrclem8  18179  fullsetcestrc  18183  prfcl  18220  prf1st  18221  prf2nd  18222  1st2ndprf  18223  curfuncf  18255  isposd  18339  lubun  18530  isacs3lem  18557  pslem  18587  psss  18595  pwsdiagmhm  18814  grpinvid1  18979  grpinvid2  18980  grplcan  18988  grpnpncan0  19024  dfgrp3lem  19026  dfgrp3  19027  grplactcnv  19031  0nsg  19157  eqger  19166  eqg0subg  19184  qus0subgadd  19187  resghm  19220  conjghm  19237  subgga  19288  gaorber  19296  gastacl  19297  orbsta  19301  symgextf1lem  19406  psgnunilem2  19481  odid  19524  odmulg  19542  gexid  19567  odcau  19590  lsmssv  19629  lsmcom2  19641  pj1ghm  19689  frgpuptf  19756  frgpup1  19761  ghmplusg  19832  cyggex2  19883  gsumval3eu  19890  gsumval3  19893  ablfac1eu  20061  pgpfac1lem5  20067  ablsimpgfind  20098  ringurd  20150  srhmsubc  20645  isdomn4  20681  isdrngd  20730  isdrngdOLD  20732  issrngd  20820  lmhmf1o  21009  lmhmima  21010  lmhmpreima  21011  lspextmo  21019  pwssplit2  21023  pwssplit3  21024  lspdisj  21091  islbs3  21121  lbsextlem4  21127  drngnidl  21209  rngqiprngghmlem2  21254  rngqiprnglinlem1  21257  rngqiprngghm  21265  lidldvgen  21300  cnsubrg  21400  znunit  21529  cygznlem3  21535  dsmmsubg  21708  dsmmlss  21709  frlmsslsp  21761  frlmup1  21763  lindfrn  21786  f1lindf  21787  issubassa2  21857  psrbagconf1o  21894  psrgrp  21921  evlslem2  22042  mhplss  22098  psdmul  22109  psdmvr  22112  ply1sclf1  22231  mamuass  22345  dmatmul  22440  dmatsubcl  22441  dmatmulcl  22443  dmatcrng  22445  scmataddcl  22459  scmatsubcl  22460  scmatcrng  22464  mdetunilem2  22556  pm2mpf1  22742  pm2mpghm  22759  eltg2  22901  ntrss  22998  opncldf1  23027  ssnei2  23059  neindisj  23060  restopnb  23118  restntr  23125  tgcmp  23344  hauscmplem  23349  2ndc1stc  23394  2ndcdisj  23399  2ndcomap  23401  restlly  23426  lly1stc  23439  isref  23452  islocfin  23460  comppfsc  23475  txcls  23547  txdis1cn  23578  pthaus  23581  txlm  23591  qtoptop2  23642  qtopomap  23661  kqt0lem  23679  pt1hmeo  23749  ptuncnv  23750  xkocnv  23757  fbasfip  23811  fgabs  23822  fbasrn  23827  elfm2  23891  fmfnfmlem2  23898  fmfnfmlem4  23900  ptcmplem3  23997  ptcmplem4  23998  tsmsres  24087  tsmsxplem1  24096  utoptop  24178  elbl2ps  24333  elbl2  24334  blin  24365  xmeter  24377  xmetresbl  24381  stdbdxmet  24459  metrest  24468  metustexhalf  24500  dscmet  24516  nrmmetd  24518  tngngp2  24596  nmoi2  24674  icccmplem2  24768  reconnlem2  24772  metdstri  24796  metdsle  24797  metdsre  24798  metnrmlem3  24806  fsumcn  24817  icccvx  24904  bndth  24913  evth  24914  reparphti  24952  reparphtiOLD  24953  pi1blem  24995  tcphcph  25194  iscfil2  25223  cfilfcls  25231  iscau4  25236  iscauf  25237  caucfil  25240  cncmet  25279  minveclem7  25392  ovoliunlem1  25460  ovolicc2lem2  25476  ovolicc2lem3  25477  ovolicc2lem4  25478  ovolicc2lem5  25479  ovolicc2  25480  voliunlem3  25510  voliun  25512  ioombl  25523  volivth  25565  ismbfd  25597  ismbf3d  25612  itg1addlem1  25650  i1fadd  25653  itg1addlem4  25657  itg2split  25707  itg2monolem1  25708  itg2gt0  25718  ibllem  25722  itgvallem3  25744  iblposlem  25750  bddiblnc  25800  dvmptfsum  25936  rolle  25951  dvlip  25955  c1liplem1  25958  lhop1  25976  lhop2  25977  dvcvx  25982  dvfsumge  25985  dvfsumrlimge0  25994  dvfsumrlim  25995  dvfsum2  25998  mdegaddle  26036  mdegvscale  26037  mdegmullem  26040  ply1divex  26099  coeeulem  26186  plyco  26203  dgrlt  26229  vieta1  26277  ulmss  26363  ulmdvlem3  26368  iblulm  26373  tanord  26504  eff1olem  26514  logdivlt  26587  logccv  26629  lawcos  26783  xrlimcnp  26935  cxp2limlem  26943  cxp2lim  26944  cxploglim2  26946  divsqrtsumo1  26951  lgambdd  27004  sqff1o  27149  dvdsppwf1o  27153  dvdsflf1o  27154  musum  27158  muinv  27160  fsumdvdsmul  27162  fsumdvdsmulOLD  27164  sgmmul  27169  fsumvma  27181  logfac2  27185  chpchtsum  27187  logfacrlim  27192  logexprlim  27193  dchrelbas3  27206  dchrmulcl  27217  bposlem1  27252  lgsdchr  27323  lgsquadlem1  27348  lgsquadlem2  27349  lgsquad2lem2  27353  chebbnd1lem1  27437  chpchtlim  27447  rplogsumlem2  27453  dchrmusum2  27462  dchrvmasumlem1  27463  dchrvmasum2lem  27464  dchrvmasumlem2  27466  dchrvmasumlem3  27467  dchrvmasumiflem2  27470  dchrisum0flb  27478  dchrisum0fno1  27479  rpvmasum2  27480  dchrisum0re  27481  dchrisum0lem1  27484  dchrisum0lem2a  27485  dchrisum0lem2  27486  dchrisum0lem3  27487  rplogsum  27495  mulogsum  27500  mulog2sumlem2  27503  vmalogdivsum2  27506  2vmadivsumlem  27508  selberglem2  27514  selberg3lem1  27525  selberg4lem1  27528  selberg4  27529  pntrsumo1  27533  selberg34r  27539  pntrlog2bndlem1  27545  pntrlog2bndlem2  27546  pntrlog2bndlem3  27547  pntrlog2bndlem4  27548  pntrlog2bndlem5  27549  pntrlog2bndlem6  27551  pntibndlem3  27560  pntlemp  27578  ostthlem1  27595  ostth3  27606  sltres  27631  noresle  27666  nosupno  27672  nosupbday  27674  noinfno  27687  bday1s  27800  cutlt  27897  addsproplem2  27934  negsproplem2  27992  mulsuniflem  28109  mulsunif2lem  28129  precsexlem9  28174  precsexlem10  28175  precsexlem11  28176  om2noseqlt  28250  om2noseqlt2  28251  om2noseqf1o  28252  om2noseqrdg  28255  noseqrdgfn  28257  recut  28404  renegscl  28406  ercgrg  28501  oppperpex  28737  axlowdimlem15  28940  axlowdimlem16  28941  axcontlem10  28957  cusgrfilem1  29440  upgriswlk  29626  crctcshwlkn0  29808  wwlksnext  29880  wwlksnextwrd  29884  clwlkclwwlklem2a  29984  wwlksext2clwwlk  30043  grpoidinv  30494  grporcan  30504  grpoinvid1  30514  grpoinvid2  30515  grpolcan  30516  ablo4  30536  nvabs  30658  minvecolem7  30869  htthlem  30903  hvadd4  31022  hvaddsub4  31064  shscli  31303  pjspansn  31563  fh1  31604  fh2  31605  cm2j  31606  chscllem2  31624  spansncvi  31638  5oalem2  31641  5oalem5  31644  5oalem6  31645  3oalem2  31649  hoadd4  31770  cnvunop  31904  bralnfn  31934  eighmorth  31950  hmops  32006  hmopm  32007  adjlnop  32072  adjmul  32078  adjadd  32079  nmopcoi  32081  kbass5  32106  kbass6  32107  hstle  32216  stlesi  32227  mdsl0  32296  mdexchi  32321  atom1d  32339  superpos  32340  cvexchlem  32354  atomli  32368  atcvatlem  32371  chirredlem2  32377  chirredlem3  32378  atcvat4i  32383  mdsymlem1  32389  mdsymlem3  32391  mdsymlem5  32393  mdsymlem6  32394  sumdmdlem  32404  sumdmdlem2  32405  cdj1i  32419  opeldifid  32585  isoun  32684  1stpreimas  32688  f1od2  32703  indf1ofs  32848  ccatf1  32929  archirngz  33192  archiabllem1  33196  archiabllem2c  33198  qusxpid  33383  esum2d  34129  cntmeas  34262  ddemeas  34272  carsgclctunlem1  34354  itgeq12dv  34363  eulerpartlemgc  34399  eulerpartlemb  34405  eulerpartlemgs2  34417  ballotlemfc0  34530  ballotlemfcc  34531  reprss  34654  reprpmtf1o  34663  hgt750lemb  34693  bnj607  34952  derangenlem  35198  subfacp1lem3  35209  subfacp1lem5  35211  cvmliftmolem2  35309  cvmliftlem6  35317  cvmlift2lem5  35334  cvmlift2lem7  35336  cvmlift2lem9  35338  mppspstlem  35598  dfon2lem6  35811  colinbtwnle  36141  finminlem  36341  nn0prpwlem  36345  isfne  36362  neibastop1  36382  neibastop2lem  36383  neibastop3  36385  tailfb  36400  onsuct0  36464  nndivsub  36480  knoppcnlem6  36521  knoppndvlem9  36543  knoppndvlem18  36552  knoppndvlem21  36555  bj-prmoore  37138  bj-finsumval0  37308  rdgeqoa  37393  pibt2  37440  lindsadd  37642  matunitlindflem2  37646  poimirlem4  37653  poimirlem11  37660  poimirlem12  37661  poimirlem13  37662  poimirlem25  37674  poimirlem28  37677  heicant  37684  mblfinlem2  37687  mblfinlem3  37688  mblfinlem4  37689  mbfposadd  37696  itg2addnclem3  37702  ftc1anclem5  37726  ftc1anclem6  37727  ftc1anclem7  37728  ftc1anc  37730  frinfm  37764  filbcmb  37769  seqpo  37776  sstotbnd2  37803  isbndx  37811  ssbnd  37817  prdsbnd  37822  ismtycnv  37831  ismtyres  37837  heiborlem3  37842  heibor  37850  ghomdiv  37921  grpokerinj  37922  isdrngo2  37987  rngohomco  38003  rngoisocnv  38010  rngoisoco  38011  crngm4  38032  crngohomfo  38035  isidlc  38044  ispridl2  38067  ispridlc  38099  prtlem16  38892  ax12eq  38964  ax12el  38965  lshpcmp  39011  omllaw3  39268  omlfh1N  39281  cvratlem  39445  cvrat3  39466  cvrat4  39467  ps-2  39502  elpaddn0  39824  paddasslem10  39853  cdleme0cp  40238  cdleme32a  40465  cdlemeg49lebilem  40563  cdleme50eq  40565  tendoeq2  40798  diaglbN  41079  diameetN  41080  diainN  41081  dvhopN  41140  djaclN  41160  djajN  41161  dihopelvalcpre  41272  dih1dimatlem  41353  dihmeetcl  41369  djhcl  41424  mapdpglem2  41697  3factsumint1  42039  sticksstones22  42186  unitscyglem4  42216  imacrhmcl  42512  frlmsnic  42538  psrmnd  42543  evlselvlem  42584  fsuppind  42588  0prjspn  42626  infdesc  42641  ismrc  42699  eldioph2  42760  lzenom  42768  rexrabdioph  42792  fphpdo  42815  irrapxlem3  42822  elpell14qr2  42860  pell14qrreccl  42862  pell14qrdich  42867  pellfundglb  42883  monotoddzzfi  42941  2nn0ind  42944  jm2.21  42993  jm2.22  42994  dnnumch3  43046  dnwech  43047  fnwe2lem2  43050  hbtlem6  43128  cantnfresb  43323  imo72b2lem1  44168  mnuprdlem1  44271  mnuprdlem2  44272  relpmin  44952  traxext  44977  cncmpmax  45036  disjf1  45187  eliccelioc  45530  fprodexp  45603  fprodabs2  45604  mullimc  45625  mullimcf  45632  islpcn  45648  limsuppnfdlem  45710  liminfval2  45777  xlimmnfvlem1  45841  xlimmnfvlem2  45842  xlimpnfvlem1  45845  xlimpnfvlem2  45846  cncfshift  45883  cncfperiod  45888  fprodcncf  45909  dvnprodlem1  45955  dvnprodlem2  45956  stoweidlem34  46043  stoweidlem48  46057  stoweidlem60  46069  fourierdlem42  46158  fourierdlem60  46175  fourierdlem61  46176  fourierdlem63  46178  fourierdlem65  46180  fourierdlem87  46202  fourierdlem97  46212  elaa2  46243  etransclem46  46289  etransc  46292  salrestss  46370  sge0iunmptlemfi  46422  isomennd  46540  ovnsslelem  46569  ovolval4lem2  46659  smflimlem3  46782  smflimlem4  46783  smflimlem6  46785  smfpimbor1lem1  46807  smflimmpt  46819  smflimsupmpt  46838  smfliminfmpt  46841  fsetsnf1  47061  fcoresf1  47078  fvelsetpreimafv  47381  icceuelpart  47430  prproropf1olem4  47500  fmtnoprmfac2  47561  bgoldbtbndlem2  47800  bgoldbtbndlem3  47801  gpgnbgrvtx0  48056  gpgnbgrvtx1  48057  gpg3nbgrvtx0ALT  48059  gpg3nbgrvtx1  48060  srhmsubcALTV  48280  catprs  48966  thincciso2  49321  prsthinc  49330  functermc  49373  fulltermc  49376  aacllem  49645