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  1131  3ad2antr1  1187  reusv2lem3  5405  axprlem4OLD  5434  otsndisj  5528  otiunsndisj  5529  po2nr  5610  sotric  5625  sotrieq  5626  tz7.7  6411  fmptsnd  7188  fvtp1g  7217  f1cofveqaeqALT  7278  fsnex  7302  isocnv  7349  isores2  7352  isomin  7356  isoini  7357  f1oiso2  7371  ovmpodf  7588  offval  7705  ordsucun  7844  xp1st  8044  cnvf1olem  8133  fnse  8156  sexp2  8169  mpoxopoveq  8242  frrlem3  8311  frrlem13  8321  wfrlem3OLD  8348  oalim  8568  omlim  8569  oaass  8597  omordi  8602  omwordri  8608  odi  8615  oen0  8622  oewordri  8628  nnawordi  8657  nnmordi  8667  omabs  8687  coflton  8707  nadd4  8734  erinxp  8829  dom2lem  9030  domssl  9036  mapen  9179  ssenen  9189  ssfiALT  9212  domfi  9226  php  9244  domunfican  9358  mapfien  9445  ordtypelem6  9560  ordtypelem7  9561  card2inf  9592  inf3lem6  9670  cantnfle  9708  cantnflem1b  9723  cantnflem1  9726  wemapwe  9734  ttrclselem2  9763  rankxplim3  9918  fseqenlem2  10062  dfac5lem4  10163  dfac5lem4OLD  10165  dfac2b  10168  cfsuc  10294  cfflb  10296  cofsmo  10306  infpssrlem4  10343  fin4en1  10346  ssfin4  10347  fin23lem26  10362  fin23lem22  10364  fin23lem27  10365  isf34lem4  10414  isf34lem5  10415  fin1a2lem12  10448  axdc3lem2  10488  axdc4lem  10492  ttukeylem6  10551  iundom2g  10577  pwcfsdom  10620  gchen2  10663  gchor  10664  fpwwe2lem6  10673  fpwwe2lem8  10675  fpwwe2lem10  10677  fpwwe2lem11  10678  fpwwe2  10680  pwfseqlem4  10699  gchina  10736  ltexprlem6  11078  prlem936  11084  mul4  11426  2addsub  11519  muladd  11692  ltleadd  11743  leord1  11787  eqord1  11788  ltord2  11789  leord2  11790  eqord2  11791  divmul3  11924  divcan7  11973  divadddiv  11979  lemul2a  12119  lemul12b  12121  ltmuldiv2  12139  ltdivmul  12140  ledivmul  12141  ltdivmul2  12142  lt2mul2div  12143  ledivmul2  12144  lemuldiv2  12146  lt2msq  12150  ltdiv23  12156  lediv23  12157  fimaxre  12209  supadd  12233  supmullem1  12235  cju  12259  zextlt  12689  suprzcl  12695  zmax  12984  xrlttr  13178  xrre3  13209  qbtwnre  13237  xrsupsslem  13345  xrinfmsslem  13346  supxrunb1  13357  supxrunb2  13358  ixxdisj  13398  iooshf  13462  icodisj  13512  iccf1o  13532  modid  13932  modadd1  13944  modmul1  13961  seqf1o  14080  expsub  14147  sqlecan  14244  bcval5  14353  hashmap  14470  hashfacen  14489  seqcoll  14499  swrdswrdlem  14738  swrdccatin2  14763  cshwidxmod  14837  2cshwcshw  14860  cshwcshid  14862  resqreu  15287  lenegsq  15355  limsupbnd2  15515  icco1  15572  rlimresb  15597  rlimsqzlem  15681  rlimsqz  15682  rlimsqz2  15683  caucvgrlem  15705  fsum0diag2  15815  o1fsum  15845  ruclem8  16269  dvdsmulcr  16319  ndvdsadd  16443  bitsshft  16508  lcmdvds  16641  hashdvds  16808  eulerthlem2  16815  phisum  16823  pcqmul  16886  pcmpt  16925  prmreclem3  16951  4sqlem11  16988  0ram  17053  ramub1  17061  invfun  17811  initoeu2lem2  18068  coaval  18121  catcisolem  18163  funcestrcsetclem8  18202  fullestrcsetc  18206  embedsetcestrclem  18212  funcsetcestrclem8  18217  fullsetcestrc  18221  prfcl  18258  prf1st  18259  prf2nd  18260  1st2ndprf  18261  curfuncf  18294  isposd  18380  lubun  18572  isacs3lem  18599  pslem  18629  psss  18637  pwsdiagmhm  18856  grpinvid1  19021  grpinvid2  19022  grplcan  19030  grpnpncan0  19066  dfgrp3lem  19068  dfgrp3  19069  grplactcnv  19073  0nsg  19199  eqger  19208  eqg0subg  19226  qus0subgadd  19229  resghm  19262  conjghm  19279  subgga  19330  gaorber  19338  gastacl  19339  orbsta  19343  symgextf1lem  19452  psgnunilem2  19527  odid  19570  odmulg  19588  gexid  19613  odcau  19636  lsmssv  19675  lsmcom2  19687  pj1ghm  19735  frgpuptf  19802  frgpup1  19807  ghmplusg  19878  cyggex2  19929  gsumval3eu  19936  gsumval3  19939  ablfac1eu  20107  pgpfac1lem5  20113  ablsimpgfind  20144  ringurd  20202  srhmsubc  20696  isdomn4  20732  isdrngd  20781  isdrngdOLD  20783  issrngd  20872  lmhmf1o  21062  lmhmima  21063  lmhmpreima  21064  lspextmo  21072  pwssplit2  21076  pwssplit3  21077  lspdisj  21144  islbs3  21174  lbsextlem4  21180  drngnidl  21270  rngqiprngghmlem2  21315  rngqiprnglinlem1  21318  rngqiprngghm  21326  lidldvgen  21361  cnsubrg  21462  znunit  21599  cygznlem3  21605  dsmmsubg  21780  dsmmlss  21781  frlmsslsp  21833  frlmup1  21835  lindfrn  21858  f1lindf  21859  issubassa2  21929  psrbagconf1o  21966  psrgrp  21993  evlslem2  22120  mhplss  22176  psdmul  22187  ply1sclf1  22307  mamuass  22421  dmatmul  22518  dmatsubcl  22519  dmatmulcl  22521  dmatcrng  22523  scmataddcl  22537  scmatsubcl  22538  scmatcrng  22542  mdetunilem2  22634  pm2mpf1  22820  pm2mpghm  22837  eltg2  22980  ntrss  23078  opncldf1  23107  ssnei2  23139  neindisj  23140  restopnb  23198  restntr  23205  tgcmp  23424  hauscmplem  23429  2ndc1stc  23474  2ndcdisj  23479  2ndcomap  23481  restlly  23506  lly1stc  23519  isref  23532  islocfin  23540  comppfsc  23555  txcls  23627  txdis1cn  23658  pthaus  23661  txlm  23671  qtoptop2  23722  qtopomap  23741  kqt0lem  23759  pt1hmeo  23829  ptuncnv  23830  xkocnv  23837  fbasfip  23891  fgabs  23902  fbasrn  23907  elfm2  23971  fmfnfmlem2  23978  fmfnfmlem4  23980  ptcmplem3  24077  ptcmplem4  24078  tsmsres  24167  tsmsxplem1  24176  utoptop  24258  elbl2ps  24414  elbl2  24415  blin  24446  xmeter  24458  xmetresbl  24462  stdbdxmet  24543  metrest  24552  metustexhalf  24584  dscmet  24600  nrmmetd  24602  tngngp2  24688  nmoi2  24766  icccmplem2  24858  reconnlem2  24862  metdstri  24886  metdsle  24887  metdsre  24888  metnrmlem3  24896  fsumcn  24907  icccvx  24994  bndth  25003  evth  25004  reparphti  25042  reparphtiOLD  25043  pi1blem  25085  tcphcph  25284  iscfil2  25313  cfilfcls  25321  iscau4  25326  iscauf  25327  caucfil  25330  cncmet  25369  minveclem7  25482  ovoliunlem1  25550  ovolicc2lem2  25566  ovolicc2lem3  25567  ovolicc2lem4  25568  ovolicc2lem5  25569  ovolicc2  25570  voliunlem3  25600  voliun  25602  ioombl  25613  volivth  25655  ismbfd  25687  ismbf3d  25702  itg1addlem1  25740  i1fadd  25743  itg1addlem4  25747  itg1addlem4OLD  25748  itg2split  25798  itg2monolem1  25799  itg2gt0  25809  ibllem  25813  itgvallem3  25835  iblposlem  25841  bddiblnc  25891  dvmptfsum  26027  rolle  26042  dvlip  26046  c1liplem1  26049  lhop1  26067  lhop2  26068  dvcvx  26073  dvfsumge  26076  dvfsumrlimge0  26085  dvfsumrlim  26086  dvfsum2  26089  mdegaddle  26127  mdegvscale  26128  mdegmullem  26131  ply1divex  26190  coeeulem  26277  plyco  26294  dgrlt  26320  vieta1  26368  ulmss  26454  ulmdvlem3  26459  iblulm  26464  tanord  26594  eff1olem  26604  logdivlt  26677  logccv  26719  lawcos  26873  xrlimcnp  27025  cxp2limlem  27033  cxp2lim  27034  cxploglim2  27036  divsqrtsumo1  27041  lgambdd  27094  sqff1o  27239  dvdsppwf1o  27243  dvdsflf1o  27244  musum  27248  muinv  27250  fsumdvdsmul  27252  fsumdvdsmulOLD  27254  sgmmul  27259  fsumvma  27271  logfac2  27275  chpchtsum  27277  logfacrlim  27282  logexprlim  27283  dchrelbas3  27296  dchrmulcl  27307  bposlem1  27342  lgsdchr  27413  lgsquadlem1  27438  lgsquadlem2  27439  lgsquad2lem2  27443  chebbnd1lem1  27527  chpchtlim  27537  rplogsumlem2  27543  dchrmusum2  27552  dchrvmasumlem1  27553  dchrvmasum2lem  27554  dchrvmasumlem2  27556  dchrvmasumlem3  27557  dchrvmasumiflem2  27560  dchrisum0flb  27568  dchrisum0fno1  27569  rpvmasum2  27570  dchrisum0re  27571  dchrisum0lem1  27574  dchrisum0lem2a  27575  dchrisum0lem2  27576  dchrisum0lem3  27577  rplogsum  27585  mulogsum  27590  mulog2sumlem2  27593  vmalogdivsum2  27596  2vmadivsumlem  27598  selberglem2  27604  selberg3lem1  27615  selberg4lem1  27618  selberg4  27619  pntrsumo1  27623  selberg34r  27629  pntrlog2bndlem1  27635  pntrlog2bndlem2  27636  pntrlog2bndlem3  27637  pntrlog2bndlem4  27638  pntrlog2bndlem5  27639  pntrlog2bndlem6  27641  pntibndlem3  27650  pntlemp  27668  ostthlem1  27685  ostth3  27696  sltres  27721  noresle  27756  nosupno  27762  nosupbday  27764  noinfno  27777  bday1s  27890  cutlt  27980  addsproplem2  28017  negsproplem2  28075  mulsuniflem  28189  mulsunif2lem  28209  precsexlem9  28253  precsexlem10  28254  precsexlem11  28255  om2noseqlt  28319  om2noseqlt2  28320  om2noseqf1o  28321  om2noseqrdg  28324  noseqrdgfn  28326  recut  28442  renegscl  28444  ercgrg  28539  oppperpex  28775  axlowdimlem15  28985  axlowdimlem16  28986  axcontlem10  29002  cusgrfilem1  29487  upgriswlk  29673  crctcshwlkn0  29850  wwlksnext  29922  wwlksnextwrd  29926  clwlkclwwlklem2a  30026  wwlksext2clwwlk  30085  grpoidinv  30536  grporcan  30546  grpoinvid1  30556  grpoinvid2  30557  grpolcan  30558  ablo4  30578  nvabs  30700  minvecolem7  30911  htthlem  30945  hvadd4  31064  hvaddsub4  31106  shscli  31345  pjspansn  31605  fh1  31646  fh2  31647  cm2j  31648  chscllem2  31666  spansncvi  31680  5oalem2  31683  5oalem5  31686  5oalem6  31687  3oalem2  31691  hoadd4  31812  cnvunop  31946  bralnfn  31976  eighmorth  31992  hmops  32048  hmopm  32049  adjlnop  32114  adjmul  32120  adjadd  32121  nmopcoi  32123  kbass5  32148  kbass6  32149  hstle  32258  stlesi  32269  mdsl0  32338  mdexchi  32363  atom1d  32381  superpos  32382  cvexchlem  32396  atomli  32410  atcvatlem  32413  chirredlem2  32419  chirredlem3  32420  atcvat4i  32425  mdsymlem1  32431  mdsymlem3  32433  mdsymlem5  32435  mdsymlem6  32436  sumdmdlem  32446  sumdmdlem2  32447  cdj1i  32461  opeldifid  32618  isoun  32716  1stpreimas  32720  f1od2  32738  ccatf1  32917  archirngz  33178  archiabllem1  33182  archiabllem2c  33184  qusxpid  33370  indf1ofs  34006  esum2d  34073  cntmeas  34206  ddemeas  34216  carsgclctunlem1  34298  itgeq12dv  34307  eulerpartlemgc  34343  eulerpartlemb  34349  eulerpartlemgs2  34361  ballotlemfc0  34473  ballotlemfcc  34474  reprss  34610  reprpmtf1o  34619  hgt750lemb  34649  bnj607  34908  derangenlem  35155  subfacp1lem3  35166  subfacp1lem5  35168  cvmliftmolem2  35266  cvmliftlem6  35274  cvmlift2lem5  35291  cvmlift2lem7  35293  cvmlift2lem9  35295  mppspstlem  35555  dfon2lem6  35769  colinbtwnle  36099  finminlem  36300  nn0prpwlem  36304  isfne  36321  neibastop1  36341  neibastop2lem  36342  neibastop3  36344  tailfb  36359  onsuct0  36423  nndivsub  36439  knoppcnlem6  36480  knoppndvlem9  36502  knoppndvlem18  36511  knoppndvlem21  36514  bj-prmoore  37097  bj-finsumval0  37267  rdgeqoa  37352  pibt2  37399  lindsadd  37599  matunitlindflem2  37603  poimirlem4  37610  poimirlem11  37617  poimirlem12  37618  poimirlem13  37619  poimirlem25  37631  poimirlem28  37634  heicant  37641  mblfinlem2  37644  mblfinlem3  37645  mblfinlem4  37646  mbfposadd  37653  itg2addnclem3  37659  ftc1anclem5  37683  ftc1anclem6  37684  ftc1anclem7  37685  ftc1anc  37687  frinfm  37721  filbcmb  37726  seqpo  37733  sstotbnd2  37760  isbndx  37768  ssbnd  37774  prdsbnd  37779  ismtycnv  37788  ismtyres  37794  heiborlem3  37799  heibor  37807  ghomdiv  37878  grpokerinj  37879  isdrngo2  37944  rngohomco  37960  rngoisocnv  37967  rngoisoco  37968  crngm4  37989  crngohomfo  37992  isidlc  38001  ispridl2  38024  ispridlc  38056  prtlem16  38850  ax12eq  38922  ax12el  38923  lshpcmp  38969  omllaw3  39226  omlfh1N  39239  cvratlem  39403  cvrat3  39424  cvrat4  39425  ps-2  39460  elpaddn0  39782  paddasslem10  39811  cdleme0cp  40196  cdleme32a  40423  cdlemeg49lebilem  40521  cdleme50eq  40523  tendoeq2  40756  diaglbN  41037  diameetN  41038  diainN  41039  dvhopN  41098  djaclN  41118  djajN  41119  dihopelvalcpre  41230  dih1dimatlem  41311  dihmeetcl  41327  djhcl  41382  mapdpglem2  41655  3factsumint1  42002  sticksstones22  42149  unitscyglem4  42179  metakunt2  42187  imacrhmcl  42500  frlmsnic  42526  psrmnd  42531  evlselvlem  42572  fsuppind  42576  0prjspn  42614  infdesc  42629  ismrc  42688  eldioph2  42749  lzenom  42757  rexrabdioph  42781  fphpdo  42804  irrapxlem3  42811  elpell14qr2  42849  pell14qrreccl  42851  pell14qrdich  42856  pellfundglb  42872  monotoddzzfi  42930  2nn0ind  42933  jm2.21  42982  jm2.22  42983  dnnumch3  43035  dnwech  43036  fnwe2lem2  43039  hbtlem6  43117  cantnfresb  43313  imo72b2lem1  44158  mnuprdlem1  44267  mnuprdlem2  44268  traxext  44937  cncmpmax  44969  disjf1  45125  eliccelioc  45473  fprodexp  45549  fprodabs2  45550  mullimc  45571  mullimcf  45578  islpcn  45594  limsuppnfdlem  45656  liminfval2  45723  xlimmnfvlem1  45787  xlimmnfvlem2  45788  xlimpnfvlem1  45791  xlimpnfvlem2  45792  cncfshift  45829  cncfperiod  45834  fprodcncf  45855  dvnprodlem1  45901  dvnprodlem2  45902  stoweidlem34  45989  stoweidlem48  46003  stoweidlem60  46015  fourierdlem42  46104  fourierdlem60  46121  fourierdlem61  46122  fourierdlem63  46124  fourierdlem65  46126  fourierdlem87  46148  fourierdlem97  46158  elaa2  46189  etransclem46  46235  etransc  46238  salrestss  46316  sge0iunmptlemfi  46368  isomennd  46486  ovnsslelem  46515  ovolval4lem2  46605  smflimlem3  46728  smflimlem4  46729  smflimlem6  46731  smfpimbor1lem1  46753  smflimmpt  46765  smflimsupmpt  46784  smfliminfmpt  46787  fsetsnf1  47001  fcoresf1  47018  fvelsetpreimafv  47311  icceuelpart  47360  prproropf1olem4  47430  fmtnoprmfac2  47491  bgoldbtbndlem2  47730  bgoldbtbndlem3  47731  gpgnbgrvtx0  47964  gpgnbgrvtx1  47965  gpg3nbgrvtx0ALT  47967  gpg3nbgrvtx1  47968  srhmsubcALTV  48168  catprs  48799  prsthinc  48854  aacllem  49031