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  5355  axprlem4OLD  5384  otsndisj  5479  otiunsndisj  5480  po2nr  5560  sotric  5576  sotrieq  5577  tz7.7  6358  fmptsnd  7143  fvtp1g  7172  f1cofveqaeqALT  7233  fsnex  7258  isocnv  7305  isores2  7308  isomin  7312  isoini  7313  f1oiso2  7327  ovmpodf  7545  offval  7662  ordsucun  7800  xp1st  8000  cnvf1olem  8089  fnse  8112  sexp2  8125  mpoxopoveq  8198  frrlem3  8267  frrlem13  8277  oalim  8496  omlim  8497  oaass  8525  omordi  8530  omwordri  8536  odi  8543  oen0  8550  oewordri  8556  nnawordi  8585  nnmordi  8595  omabs  8615  coflton  8635  nadd4  8662  erinxp  8764  dom2lem  8963  domssl  8969  mapen  9105  ssenen  9115  ssfiALT  9138  domfi  9153  php  9171  domunfican  9272  mapfien  9359  ordtypelem6  9476  ordtypelem7  9477  card2inf  9508  inf3lem6  9586  cantnfle  9624  cantnflem1b  9639  cantnflem1  9642  wemapwe  9650  ttrclselem2  9679  rankxplim3  9834  fseqenlem2  9978  dfac5lem4  10079  dfac5lem4OLD  10081  dfac2b  10084  cfsuc  10210  cfflb  10212  cofsmo  10222  infpssrlem4  10259  fin4en1  10262  ssfin4  10263  fin23lem26  10278  fin23lem22  10280  fin23lem27  10281  isf34lem4  10330  isf34lem5  10331  fin1a2lem12  10364  axdc3lem2  10404  axdc4lem  10408  ttukeylem6  10467  iundom2g  10493  pwcfsdom  10536  gchen2  10579  gchor  10580  fpwwe2lem6  10589  fpwwe2lem8  10591  fpwwe2lem10  10593  fpwwe2lem11  10594  fpwwe2  10596  pwfseqlem4  10615  gchina  10652  ltexprlem6  10994  prlem936  11000  mul4  11342  2addsub  11435  muladd  11610  ltleadd  11661  leord1  11705  eqord1  11706  ltord2  11707  leord2  11708  eqord2  11709  divmul3  11842  divcan7  11891  divadddiv  11897  lemul2a  12037  lemul12b  12039  ltmuldiv2  12057  ltdivmul  12058  ledivmul  12059  ltdivmul2  12060  lt2mul2div  12061  ledivmul2  12062  lemuldiv2  12064  lt2msq  12068  ltdiv23  12074  lediv23  12075  fimaxre  12127  supadd  12151  supmullem1  12153  cju  12182  zextlt  12608  suprzcl  12614  zmax  12904  xrlttr  13100  xrre3  13131  qbtwnre  13159  xrsupsslem  13267  xrinfmsslem  13268  supxrunb1  13279  supxrunb2  13280  ixxdisj  13321  iooshf  13387  icodisj  13437  iccf1o  13457  modid  13858  modadd1  13870  modmul1  13889  seqf1o  14008  expsub  14075  sqlecan  14174  bcval5  14283  hashmap  14400  hashfacen  14419  seqcoll  14429  swrdswrdlem  14669  swrdccatin2  14694  cshwidxmod  14768  2cshwcshw  14791  cshwcshid  14793  resqreu  15218  lenegsq  15287  limsupbnd2  15449  icco1  15506  rlimresb  15531  rlimsqzlem  15615  rlimsqz  15616  rlimsqz2  15617  caucvgrlem  15639  fsum0diag2  15749  o1fsum  15779  ruclem8  16205  dvdsmulcr  16255  ndvdsadd  16380  bitsshft  16445  lcmdvds  16578  hashdvds  16745  eulerthlem2  16752  phisum  16761  pcqmul  16824  pcmpt  16863  prmreclem3  16889  4sqlem11  16926  0ram  16991  ramub1  16999  invfun  17726  initoeu2lem2  17977  coaval  18030  catcisolem  18072  funcestrcsetclem8  18108  fullestrcsetc  18112  embedsetcestrclem  18118  funcsetcestrclem8  18123  fullsetcestrc  18127  prfcl  18164  prf1st  18165  prf2nd  18166  1st2ndprf  18167  curfuncf  18199  isposd  18283  lubun  18474  isacs3lem  18501  pslem  18531  psss  18539  pwsdiagmhm  18758  grpinvid1  18923  grpinvid2  18924  grplcan  18932  grpnpncan0  18968  dfgrp3lem  18970  dfgrp3  18971  grplactcnv  18975  0nsg  19101  eqger  19110  eqg0subg  19128  qus0subgadd  19131  resghm  19164  conjghm  19181  subgga  19232  gaorber  19240  gastacl  19241  orbsta  19245  symgextf1lem  19350  psgnunilem2  19425  odid  19468  odmulg  19486  gexid  19511  odcau  19534  lsmssv  19573  lsmcom2  19585  pj1ghm  19633  frgpuptf  19700  frgpup1  19705  ghmplusg  19776  cyggex2  19827  gsumval3eu  19834  gsumval3  19837  ablfac1eu  20005  pgpfac1lem5  20011  ablsimpgfind  20042  ringurd  20094  srhmsubc  20589  isdomn4  20625  isdrngd  20674  isdrngdOLD  20676  issrngd  20764  lmhmf1o  20953  lmhmima  20954  lmhmpreima  20955  lspextmo  20963  pwssplit2  20967  pwssplit3  20968  lspdisj  21035  islbs3  21065  lbsextlem4  21071  drngnidl  21153  rngqiprngghmlem2  21198  rngqiprnglinlem1  21201  rngqiprngghm  21209  lidldvgen  21244  cnsubrg  21344  znunit  21473  cygznlem3  21479  dsmmsubg  21652  dsmmlss  21653  frlmsslsp  21705  frlmup1  21707  lindfrn  21730  f1lindf  21731  issubassa2  21801  psrbagconf1o  21838  psrgrp  21865  evlslem2  21986  mhplss  22042  psdmul  22053  psdmvr  22056  ply1sclf1  22175  mamuass  22289  dmatmul  22384  dmatsubcl  22385  dmatmulcl  22387  dmatcrng  22389  scmataddcl  22403  scmatsubcl  22404  scmatcrng  22408  mdetunilem2  22500  pm2mpf1  22686  pm2mpghm  22703  eltg2  22845  ntrss  22942  opncldf1  22971  ssnei2  23003  neindisj  23004  restopnb  23062  restntr  23069  tgcmp  23288  hauscmplem  23293  2ndc1stc  23338  2ndcdisj  23343  2ndcomap  23345  restlly  23370  lly1stc  23383  isref  23396  islocfin  23404  comppfsc  23419  txcls  23491  txdis1cn  23522  pthaus  23525  txlm  23535  qtoptop2  23586  qtopomap  23605  kqt0lem  23623  pt1hmeo  23693  ptuncnv  23694  xkocnv  23701  fbasfip  23755  fgabs  23766  fbasrn  23771  elfm2  23835  fmfnfmlem2  23842  fmfnfmlem4  23844  ptcmplem3  23941  ptcmplem4  23942  tsmsres  24031  tsmsxplem1  24040  utoptop  24122  elbl2ps  24277  elbl2  24278  blin  24309  xmeter  24321  xmetresbl  24325  stdbdxmet  24403  metrest  24412  metustexhalf  24444  dscmet  24460  nrmmetd  24462  tngngp2  24540  nmoi2  24618  icccmplem2  24712  reconnlem2  24716  metdstri  24740  metdsle  24741  metdsre  24742  metnrmlem3  24750  fsumcn  24761  icccvx  24848  bndth  24857  evth  24858  reparphti  24896  reparphtiOLD  24897  pi1blem  24939  tcphcph  25137  iscfil2  25166  cfilfcls  25174  iscau4  25179  iscauf  25180  caucfil  25183  cncmet  25222  minveclem7  25335  ovoliunlem1  25403  ovolicc2lem2  25419  ovolicc2lem3  25420  ovolicc2lem4  25421  ovolicc2lem5  25422  ovolicc2  25423  voliunlem3  25453  voliun  25455  ioombl  25466  volivth  25508  ismbfd  25540  ismbf3d  25555  itg1addlem1  25593  i1fadd  25596  itg1addlem4  25600  itg2split  25650  itg2monolem1  25651  itg2gt0  25661  ibllem  25665  itgvallem3  25687  iblposlem  25693  bddiblnc  25743  dvmptfsum  25879  rolle  25894  dvlip  25898  c1liplem1  25901  lhop1  25919  lhop2  25920  dvcvx  25925  dvfsumge  25928  dvfsumrlimge0  25937  dvfsumrlim  25938  dvfsum2  25941  mdegaddle  25979  mdegvscale  25980  mdegmullem  25983  ply1divex  26042  coeeulem  26129  plyco  26146  dgrlt  26172  vieta1  26220  ulmss  26306  ulmdvlem3  26311  iblulm  26316  tanord  26447  eff1olem  26457  logdivlt  26530  logccv  26572  lawcos  26726  xrlimcnp  26878  cxp2limlem  26886  cxp2lim  26887  cxploglim2  26889  divsqrtsumo1  26894  lgambdd  26947  sqff1o  27092  dvdsppwf1o  27096  dvdsflf1o  27097  musum  27101  muinv  27103  fsumdvdsmul  27105  fsumdvdsmulOLD  27107  sgmmul  27112  fsumvma  27124  logfac2  27128  chpchtsum  27130  logfacrlim  27135  logexprlim  27136  dchrelbas3  27149  dchrmulcl  27160  bposlem1  27195  lgsdchr  27266  lgsquadlem1  27291  lgsquadlem2  27292  lgsquad2lem2  27296  chebbnd1lem1  27380  chpchtlim  27390  rplogsumlem2  27396  dchrmusum2  27405  dchrvmasumlem1  27406  dchrvmasum2lem  27407  dchrvmasumlem2  27409  dchrvmasumlem3  27410  dchrvmasumiflem2  27413  dchrisum0flb  27421  dchrisum0fno1  27422  rpvmasum2  27423  dchrisum0re  27424  dchrisum0lem1  27427  dchrisum0lem2a  27428  dchrisum0lem2  27429  dchrisum0lem3  27430  rplogsum  27438  mulogsum  27443  mulog2sumlem2  27446  vmalogdivsum2  27449  2vmadivsumlem  27451  selberglem2  27457  selberg3lem1  27468  selberg4lem1  27471  selberg4  27472  pntrsumo1  27476  selberg34r  27482  pntrlog2bndlem1  27488  pntrlog2bndlem2  27489  pntrlog2bndlem3  27490  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  pntrlog2bndlem6  27494  pntibndlem3  27503  pntlemp  27521  ostthlem1  27538  ostth3  27549  sltres  27574  noresle  27609  nosupno  27615  nosupbday  27617  noinfno  27630  bday1s  27743  cutlt  27840  addsproplem2  27877  negsproplem2  27935  mulsuniflem  28052  mulsunif2lem  28072  precsexlem9  28117  precsexlem10  28118  precsexlem11  28119  om2noseqlt  28193  om2noseqlt2  28194  om2noseqf1o  28195  om2noseqrdg  28198  noseqrdgfn  28200  recut  28347  renegscl  28349  ercgrg  28444  oppperpex  28680  axlowdimlem15  28883  axlowdimlem16  28884  axcontlem10  28900  cusgrfilem1  29383  upgriswlk  29569  crctcshwlkn0  29751  wwlksnext  29823  wwlksnextwrd  29827  clwlkclwwlklem2a  29927  wwlksext2clwwlk  29986  grpoidinv  30437  grporcan  30447  grpoinvid1  30457  grpoinvid2  30458  grpolcan  30459  ablo4  30479  nvabs  30601  minvecolem7  30812  htthlem  30846  hvadd4  30965  hvaddsub4  31007  shscli  31246  pjspansn  31506  fh1  31547  fh2  31548  cm2j  31549  chscllem2  31567  spansncvi  31581  5oalem2  31584  5oalem5  31587  5oalem6  31588  3oalem2  31592  hoadd4  31713  cnvunop  31847  bralnfn  31877  eighmorth  31893  hmops  31949  hmopm  31950  adjlnop  32015  adjmul  32021  adjadd  32022  nmopcoi  32024  kbass5  32049  kbass6  32050  hstle  32159  stlesi  32170  mdsl0  32239  mdexchi  32264  atom1d  32282  superpos  32283  cvexchlem  32297  atomli  32311  atcvatlem  32314  chirredlem2  32320  chirredlem3  32321  atcvat4i  32326  mdsymlem1  32332  mdsymlem3  32334  mdsymlem5  32336  mdsymlem6  32337  sumdmdlem  32347  sumdmdlem2  32348  cdj1i  32362  opeldifid  32528  isoun  32625  1stpreimas  32629  f1od2  32644  indf1ofs  32789  ccatf1  32870  archirngz  33143  archiabllem1  33147  archiabllem2c  33149  qusxpid  33334  esum2d  34083  cntmeas  34216  ddemeas  34226  carsgclctunlem1  34308  itgeq12dv  34317  eulerpartlemgc  34353  eulerpartlemb  34359  eulerpartlemgs2  34371  ballotlemfc0  34484  ballotlemfcc  34485  reprss  34608  reprpmtf1o  34617  hgt750lemb  34647  bnj607  34906  derangenlem  35158  subfacp1lem3  35169  subfacp1lem5  35171  cvmliftmolem2  35269  cvmliftlem6  35277  cvmlift2lem5  35294  cvmlift2lem7  35296  cvmlift2lem9  35298  mppspstlem  35558  dfon2lem6  35776  colinbtwnle  36106  finminlem  36306  nn0prpwlem  36310  isfne  36327  neibastop1  36347  neibastop2lem  36348  neibastop3  36350  tailfb  36365  onsuct0  36429  nndivsub  36445  knoppcnlem6  36486  knoppndvlem9  36508  knoppndvlem18  36517  knoppndvlem21  36520  bj-prmoore  37103  bj-finsumval0  37273  rdgeqoa  37358  pibt2  37405  lindsadd  37607  matunitlindflem2  37611  poimirlem4  37618  poimirlem11  37625  poimirlem12  37626  poimirlem13  37627  poimirlem25  37639  poimirlem28  37642  heicant  37649  mblfinlem2  37652  mblfinlem3  37653  mblfinlem4  37654  mbfposadd  37661  itg2addnclem3  37667  ftc1anclem5  37691  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anc  37695  frinfm  37729  filbcmb  37734  seqpo  37741  sstotbnd2  37768  isbndx  37776  ssbnd  37782  prdsbnd  37787  ismtycnv  37796  ismtyres  37802  heiborlem3  37807  heibor  37815  ghomdiv  37886  grpokerinj  37887  isdrngo2  37952  rngohomco  37968  rngoisocnv  37975  rngoisoco  37976  crngm4  37997  crngohomfo  38000  isidlc  38009  ispridl2  38032  ispridlc  38064  prtlem16  38862  ax12eq  38934  ax12el  38935  lshpcmp  38981  omllaw3  39238  omlfh1N  39251  cvratlem  39415  cvrat3  39436  cvrat4  39437  ps-2  39472  elpaddn0  39794  paddasslem10  39823  cdleme0cp  40208  cdleme32a  40435  cdlemeg49lebilem  40533  cdleme50eq  40535  tendoeq2  40768  diaglbN  41049  diameetN  41050  diainN  41051  dvhopN  41110  djaclN  41130  djajN  41131  dihopelvalcpre  41242  dih1dimatlem  41323  dihmeetcl  41339  djhcl  41394  mapdpglem2  41667  3factsumint1  42009  sticksstones22  42156  unitscyglem4  42186  imacrhmcl  42502  frlmsnic  42528  psrmnd  42533  evlselvlem  42574  fsuppind  42578  0prjspn  42616  infdesc  42631  ismrc  42689  eldioph2  42750  lzenom  42758  rexrabdioph  42782  fphpdo  42805  irrapxlem3  42812  elpell14qr2  42850  pell14qrreccl  42852  pell14qrdich  42857  pellfundglb  42873  monotoddzzfi  42931  2nn0ind  42934  jm2.21  42983  jm2.22  42984  dnnumch3  43036  dnwech  43037  fnwe2lem2  43040  hbtlem6  43118  cantnfresb  43313  imo72b2lem1  44158  mnuprdlem1  44261  mnuprdlem2  44262  relpmin  44942  traxext  44967  cncmpmax  45026  disjf1  45177  eliccelioc  45519  fprodexp  45592  fprodabs2  45593  mullimc  45614  mullimcf  45621  islpcn  45637  limsuppnfdlem  45699  liminfval2  45766  xlimmnfvlem1  45830  xlimmnfvlem2  45831  xlimpnfvlem1  45834  xlimpnfvlem2  45835  cncfshift  45872  cncfperiod  45877  fprodcncf  45898  dvnprodlem1  45944  dvnprodlem2  45945  stoweidlem34  46032  stoweidlem48  46046  stoweidlem60  46058  fourierdlem42  46147  fourierdlem60  46164  fourierdlem61  46165  fourierdlem63  46167  fourierdlem65  46169  fourierdlem87  46191  fourierdlem97  46201  elaa2  46232  etransclem46  46278  etransc  46281  salrestss  46359  sge0iunmptlemfi  46411  isomennd  46529  ovnsslelem  46558  ovolval4lem2  46648  smflimlem3  46771  smflimlem4  46772  smflimlem6  46774  smfpimbor1lem1  46796  smflimmpt  46808  smflimsupmpt  46827  smfliminfmpt  46830  fsetsnf1  47053  fcoresf1  47070  fvelsetpreimafv  47388  icceuelpart  47437  prproropf1olem4  47507  fmtnoprmfac2  47568  bgoldbtbndlem2  47807  bgoldbtbndlem3  47808  gpgnbgrvtx0  48065  gpgnbgrvtx1  48066  gpg3nbgrvtx0ALT  48068  gpg3nbgrvtx1  48069  srhmsubcALTV  48313  xpco2  48845  catprs  49000  uppropd  49170  thincciso2  49444  prsthinc  49453  functermc  49497  fulltermc  49500  lmdran  49660  cmdlan  49661  aacllem  49790