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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  ad2antrl  728  ad2ant2r  747  ad2ant2lr  748  cases2ALT  1049  consensus  1053  3adant3  1134  3ad2antr1  1190  reusv2lem3  5293  axprlem4  5319  otsndisj  5402  otiunsndisj  5403  po2nr  5482  sotric  5496  sotrieq  5497  tz7.7  6239  fmptsnd  6984  fvtp1g  7013  f1cofveqaeqALT  7071  fsnex  7093  isocnv  7139  isores2  7142  isomin  7146  isoini  7147  f1oiso2  7161  ovmpodf  7365  offval  7477  ordsucun  7604  xp1st  7793  cnvf1olem  7878  fnse  7900  mpoxopoveq  7961  frrlem3  8029  frrlem13  8039  wfrlem3  8056  oalim  8259  omlim  8260  oaass  8289  omordi  8294  omwordri  8300  odi  8307  oen0  8314  oewordri  8320  nnawordi  8349  nnmordi  8359  omabs  8376  erinxp  8473  dom2lem  8668  mapen  8810  ssenen  8820  ssfiALT  8852  domfi  8896  domunfican  8944  mapfien  9024  ordtypelem6  9139  ordtypelem7  9140  card2inf  9171  inf3lem6  9248  cantnfle  9286  cantnflem1b  9301  cantnflem1  9304  wemapwe  9312  rankxplim3  9497  fseqenlem2  9639  dfac5lem4  9740  dfac2b  9744  cfsuc  9871  cfflb  9873  cofsmo  9883  infpssrlem4  9920  fin4en1  9923  ssfin4  9924  fin23lem26  9939  fin23lem22  9941  fin23lem27  9942  isf34lem4  9991  isf34lem5  9992  fin1a2lem12  10025  axdc3lem2  10065  axdc4lem  10069  ttukeylem6  10128  iundom2g  10154  pwcfsdom  10197  gchen2  10240  gchor  10241  fpwwe2lem6  10250  fpwwe2lem8  10252  fpwwe2lem10  10254  fpwwe2lem11  10255  fpwwe2  10257  pwfseqlem4  10276  gchina  10313  ltexprlem6  10655  prlem936  10661  mul4  11000  2addsub  11092  muladd  11264  ltleadd  11315  leord1  11359  eqord1  11360  ltord2  11361  leord2  11362  eqord2  11363  divmul3  11495  divcan7  11541  divadddiv  11547  lemul2a  11687  lemul12b  11689  ltmuldiv2  11706  ltdivmul  11707  ledivmul  11708  ltdivmul2  11709  lt2mul2div  11710  ledivmul2  11711  lemuldiv2  11713  lt2msq  11717  ltdiv23  11723  lediv23  11724  fimaxre  11776  supadd  11800  supmullem1  11802  cju  11826  zextlt  12251  suprzcl  12257  zmax  12541  xrlttr  12730  xrre3  12761  qbtwnre  12789  xrsupsslem  12897  xrinfmsslem  12898  supxrunb1  12909  supxrunb2  12910  ixxdisj  12950  iooshf  13014  icodisj  13064  iccf1o  13084  modid  13469  modadd1  13481  modmul1  13497  seqf1o  13617  expsub  13683  sqlecan  13777  bcval5  13884  hashmap  14002  hashfacen  14018  hashfacenOLD  14019  seqcoll  14030  swrdswrdlem  14269  swrdccatin2  14294  cshwidxmod  14368  2cshwcshw  14390  cshwcshid  14392  resqreu  14816  lenegsq  14884  limsupbnd2  15044  icco1  15101  rlimresb  15126  rlimsqzlem  15212  rlimsqz  15213  rlimsqz2  15214  caucvgrlem  15236  fsum0diag2  15347  o1fsum  15377  ruclem8  15798  dvdsmulcr  15847  ndvdsadd  15971  bitsshft  16034  lcmdvds  16165  hashdvds  16328  eulerthlem2  16335  phisum  16343  pcqmul  16406  pcmpt  16445  prmreclem3  16471  4sqlem11  16508  0ram  16573  ramub1  16581  invfun  17269  initoeu2lem2  17521  coaval  17574  catcisolem  17616  funcestrcsetclem8  17654  fullestrcsetc  17658  embedsetcestrclem  17664  funcsetcestrclem8  17669  fullsetcestrc  17673  prfcl  17710  prf1st  17711  prf2nd  17712  1st2ndprf  17713  curfuncf  17746  isposd  17830  lubun  18021  isacs3lem  18048  pslem  18078  psss  18086  pwsdiagmhm  18257  gsumccatOLD  18267  grpinvid1  18418  grpinvid2  18419  grplcan  18425  grpnpncan0  18459  dfgrp3lem  18461  dfgrp3  18462  grplactcnv  18466  0nsg  18585  eqger  18594  resghm  18638  conjghm  18653  subgga  18694  gaorber  18702  gastacl  18703  orbsta  18707  symgextf1lem  18812  psgnunilem2  18887  odid  18930  odmulg  18947  gexid  18970  odcau  18993  lsmssv  19032  lsmcom2  19044  pj1ghm  19093  frgpuptf  19160  frgpup1  19165  ghmplusg  19231  cyggex2  19282  gsumval3eu  19289  gsumval3  19292  ablfac1eu  19460  pgpfac1lem5  19466  ablsimpgfind  19497  isdrngd  19792  issrngd  19897  lmhmf1o  20083  lmhmima  20084  lmhmpreima  20085  lspextmo  20093  pwssplit2  20097  pwssplit3  20098  lspdisj  20162  islbs3  20192  lbsextlem4  20198  drngnidl  20267  lidldvgen  20293  cnsubrg  20423  znunit  20528  cygznlem3  20534  dsmmsubg  20705  dsmmlss  20706  frlmsslsp  20758  frlmup1  20760  lindfrn  20783  f1lindf  20784  issubassa2  20852  psrbagconf1o  20895  psrbagconf1oOLD  20896  evlslem2  21039  mhplss  21095  ply1sclf1  21210  mamuass  21299  dmatmul  21394  dmatsubcl  21395  dmatmulcl  21397  dmatcrng  21399  scmataddcl  21413  scmatsubcl  21414  scmatcrng  21418  mdetunilem2  21510  pm2mpf1  21696  pm2mpghm  21713  eltg2  21855  ntrss  21952  opncldf1  21981  ssnei2  22013  neindisj  22014  restopnb  22072  restntr  22079  tgcmp  22298  hauscmplem  22303  2ndc1stc  22348  2ndcdisj  22353  2ndcomap  22355  restlly  22380  lly1stc  22393  isref  22406  islocfin  22414  comppfsc  22429  txcls  22501  txdis1cn  22532  pthaus  22535  txlm  22545  qtoptop2  22596  qtopomap  22615  kqt0lem  22633  pt1hmeo  22703  ptuncnv  22704  xkocnv  22711  fbasfip  22765  fgabs  22776  fbasrn  22781  elfm2  22845  fmfnfmlem2  22852  fmfnfmlem4  22854  ptcmplem3  22951  ptcmplem4  22952  tsmsres  23041  tsmsxplem1  23050  utoptop  23132  elbl2ps  23287  elbl2  23288  blin  23319  xmeter  23331  xmetresbl  23335  stdbdxmet  23413  metrest  23422  metustexhalf  23454  dscmet  23470  nrmmetd  23472  tngngp2  23550  nmoi2  23628  icccmplem2  23720  reconnlem2  23724  metdstri  23748  metdsle  23749  metdsre  23750  metnrmlem3  23758  fsumcn  23767  icccvx  23847  bndth  23855  evth  23856  reparphti  23894  pi1blem  23936  tcphcph  24134  iscfil2  24163  cfilfcls  24171  iscau4  24176  iscauf  24177  caucfil  24180  cncmet  24219  minveclem7  24332  ovoliunlem1  24399  ovolicc2lem2  24415  ovolicc2lem3  24416  ovolicc2lem4  24417  ovolicc2lem5  24418  ovolicc2  24419  voliunlem3  24449  voliun  24451  ioombl  24462  volivth  24504  ismbfd  24536  ismbf3d  24551  itg1addlem1  24589  i1fadd  24592  itg1addlem4  24596  itg1addlem4OLD  24597  itg2split  24647  itg2monolem1  24648  itg2gt0  24658  ibllem  24662  itgvallem3  24683  iblposlem  24689  bddiblnc  24739  dvmptfsum  24872  rolle  24887  dvlip  24890  c1liplem1  24893  lhop1  24911  lhop2  24912  dvcvx  24917  dvfsumge  24919  dvfsumrlimge0  24927  dvfsumrlim  24928  dvfsum2  24931  mdegaddle  24972  mdegvscale  24973  mdegmullem  24976  ply1divex  25034  coeeulem  25118  plyco  25135  dgrlt  25160  vieta1  25205  ulmss  25289  ulmdvlem3  25294  iblulm  25299  tanord  25427  eff1olem  25437  logdivlt  25509  logccv  25551  lawcos  25699  xrlimcnp  25851  cxp2limlem  25858  cxp2lim  25859  cxploglim2  25861  divsqrtsumo1  25866  lgambdd  25919  sqff1o  26064  dvdsppwf1o  26068  dvdsflf1o  26069  musum  26073  muinv  26075  fsumdvdsmul  26077  sgmmul  26082  fsumvma  26094  logfac2  26098  chpchtsum  26100  logfacrlim  26105  logexprlim  26106  dchrelbas3  26119  dchrmulcl  26130  bposlem1  26165  lgsdchr  26236  lgsquadlem1  26261  lgsquadlem2  26262  lgsquad2lem2  26266  chebbnd1lem1  26350  chpchtlim  26360  rplogsumlem2  26366  dchrmusum2  26375  dchrvmasumlem1  26376  dchrvmasum2lem  26377  dchrvmasumlem2  26379  dchrvmasumlem3  26380  dchrvmasumiflem2  26383  dchrisum0flb  26391  dchrisum0fno1  26392  rpvmasum2  26393  dchrisum0re  26394  dchrisum0lem1  26397  dchrisum0lem2a  26398  dchrisum0lem2  26399  dchrisum0lem3  26400  rplogsum  26408  mulogsum  26413  mulog2sumlem2  26416  vmalogdivsum2  26419  2vmadivsumlem  26421  selberglem2  26427  selberg3lem1  26438  selberg4lem1  26441  selberg4  26442  pntrsumo1  26446  selberg34r  26452  pntrlog2bndlem1  26458  pntrlog2bndlem2  26459  pntrlog2bndlem3  26460  pntrlog2bndlem4  26461  pntrlog2bndlem5  26462  pntrlog2bndlem6  26464  pntibndlem3  26473  pntlemp  26491  ostthlem1  26508  ostth3  26519  ercgrg  26608  oppperpex  26844  axlowdimlem15  27047  axlowdimlem16  27048  axcontlem10  27064  cusgrfilem1  27543  upgriswlk  27728  crctcshwlkn0  27905  wwlksnext  27977  wwlksnextwrd  27981  clwlkclwwlklem2a  28081  wwlksext2clwwlk  28140  grpoidinv  28589  grporcan  28599  grpoinvid1  28609  grpoinvid2  28610  grpolcan  28611  ablo4  28631  nvabs  28753  minvecolem7  28964  htthlem  28998  hvadd4  29117  hvaddsub4  29159  shscli  29398  pjspansn  29658  fh1  29699  fh2  29700  cm2j  29701  chscllem2  29719  spansncvi  29733  5oalem2  29736  5oalem5  29739  5oalem6  29740  3oalem2  29744  hoadd4  29865  cnvunop  29999  bralnfn  30029  eighmorth  30045  hmops  30101  hmopm  30102  adjlnop  30167  adjmul  30173  adjadd  30174  nmopcoi  30176  kbass5  30201  kbass6  30202  hstle  30311  stlesi  30322  mdsl0  30391  mdexchi  30416  atom1d  30434  superpos  30435  cvexchlem  30449  atomli  30463  atcvatlem  30466  chirredlem2  30472  chirredlem3  30473  atcvat4i  30478  mdsymlem1  30484  mdsymlem3  30486  mdsymlem5  30488  mdsymlem6  30489  sumdmdlem  30499  sumdmdlem2  30500  cdj1i  30514  opeldifid  30657  isoun  30754  1stpreimas  30758  f1od2  30776  ccatf1  30943  archirngz  31162  archiabllem1  31166  archiabllem2c  31168  rngurd  31201  qusxpid  31273  indf1ofs  31706  esum2d  31773  cntmeas  31906  ddemeas  31916  carsgclctunlem1  31996  itgeq12dv  32005  eulerpartlemgc  32041  eulerpartlemb  32047  eulerpartlemgs2  32059  ballotlemfc0  32171  ballotlemfcc  32172  reprss  32309  reprpmtf1o  32318  hgt750lemb  32348  bnj607  32609  derangenlem  32846  subfacp1lem3  32857  subfacp1lem5  32859  cvmliftmolem2  32957  cvmliftlem6  32965  cvmlift2lem5  32982  cvmlift2lem7  32984  cvmlift2lem9  32986  mppspstlem  33246  dfon2lem6  33483  sexp2  33530  sltres  33602  noresle  33637  nosupno  33643  nosupbday  33645  noinfno  33658  bday1s  33762  colinbtwnle  34157  finminlem  34244  nn0prpwlem  34248  isfne  34265  neibastop1  34285  neibastop2lem  34286  neibastop3  34288  tailfb  34303  onsuct0  34367  nndivsub  34383  knoppcnlem6  34415  knoppndvlem9  34437  knoppndvlem18  34446  knoppndvlem21  34449  bj-prmoore  35021  bj-finsumval0  35191  rdgeqoa  35278  pibt2  35325  lindsadd  35507  matunitlindflem2  35511  poimirlem4  35518  poimirlem11  35525  poimirlem12  35526  poimirlem13  35527  poimirlem25  35539  poimirlem28  35542  heicant  35549  mblfinlem2  35552  mblfinlem3  35553  mblfinlem4  35554  mbfposadd  35561  itg2addnclem3  35567  ftc1anclem5  35591  ftc1anclem6  35592  ftc1anclem7  35593  ftc1anc  35595  frinfm  35630  filbcmb  35635  seqpo  35642  sstotbnd2  35669  isbndx  35677  ssbnd  35683  prdsbnd  35688  ismtycnv  35697  ismtyres  35703  heiborlem3  35708  heibor  35716  ghomdiv  35787  grpokerinj  35788  isdrngo2  35853  rngohomco  35869  rngoisocnv  35876  rngoisoco  35877  crngm4  35898  crngohomfo  35901  isidlc  35910  ispridl2  35933  ispridlc  35965  prtlem16  36620  ax12eq  36692  ax12el  36693  lshpcmp  36739  omllaw3  36996  omlfh1N  37009  cvratlem  37172  cvrat3  37193  cvrat4  37194  ps-2  37229  elpaddn0  37551  paddasslem10  37580  cdleme0cp  37965  cdleme32a  38192  cdlemeg49lebilem  38290  cdleme50eq  38292  tendoeq2  38525  diaglbN  38806  diameetN  38807  diainN  38808  dvhopN  38867  djaclN  38887  djajN  38888  dihopelvalcpre  38999  dih1dimatlem  39080  dihmeetcl  39096  djhcl  39151  mapdpglem2  39424  3factsumint1  39763  sticksstones22  39846  metakunt2  39848  isdomn4  39894  frlmsnic  39975  fsuppind  39989  mhphf  39995  0prjspn  40173  infdesc  40183  ismrc  40226  eldioph2  40287  lzenom  40295  rexrabdioph  40319  fphpdo  40342  irrapxlem3  40349  elpell14qr2  40387  pell14qrreccl  40389  pell14qrdich  40394  pellfundglb  40410  monotoddzzfi  40467  2nn0ind  40470  jm2.21  40519  jm2.22  40520  dnnumch3  40575  dnwech  40576  fnwe2lem2  40579  hbtlem6  40657  imo72b2lem1  41457  mnuprdlem1  41563  mnuprdlem2  41564  cncmpmax  42248  disjf1  42393  eliccelioc  42734  fprodexp  42810  fprodabs2  42811  mullimc  42832  mullimcf  42839  islpcn  42855  limsuppnfdlem  42917  liminfval2  42984  xlimmnfvlem1  43048  xlimmnfvlem2  43049  xlimpnfvlem1  43052  xlimpnfvlem2  43053  cncfshift  43090  cncfperiod  43095  fprodcncf  43116  dvnprodlem1  43162  dvnprodlem2  43163  stoweidlem34  43250  stoweidlem48  43264  stoweidlem60  43276  fourierdlem42  43365  fourierdlem60  43382  fourierdlem61  43383  fourierdlem63  43385  fourierdlem65  43387  fourierdlem87  43409  fourierdlem97  43419  elaa2  43450  etransclem46  43496  etransc  43499  sge0iunmptlemfi  43626  isomennd  43744  ovnsslelem  43773  ovolval4lem2  43863  ovolval5lem3  43867  smflimlem3  43980  smflimlem4  43981  smflimlem6  43983  smfpimbor1lem1  44004  smflimmpt  44015  smflimsupmpt  44034  smfliminfmpt  44037  fsetsnf1  44218  fcoresf1  44235  fvelsetpreimafv  44512  icceuelpart  44561  prproropf1olem4  44631  fmtnoprmfac2  44692  bgoldbtbndlem2  44931  bgoldbtbndlem3  44932  srhmsubc  45307  srhmsubcALTV  45325  catprs  45965  prsthinc  46008  aacllem  46176