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  5358  axprlem4OLD  5387  otsndisj  5482  otiunsndisj  5483  po2nr  5563  sotric  5579  sotrieq  5580  tz7.7  6361  fmptsnd  7146  fvtp1g  7175  f1cofveqaeqALT  7236  fsnex  7261  isocnv  7308  isores2  7311  isomin  7315  isoini  7316  f1oiso2  7330  ovmpodf  7548  offval  7665  ordsucun  7803  xp1st  8003  cnvf1olem  8092  fnse  8115  sexp2  8128  mpoxopoveq  8201  frrlem3  8270  frrlem13  8280  oalim  8499  omlim  8500  oaass  8528  omordi  8533  omwordri  8539  odi  8546  oen0  8553  oewordri  8559  nnawordi  8588  nnmordi  8598  omabs  8618  coflton  8638  nadd4  8665  erinxp  8767  dom2lem  8966  domssl  8972  mapen  9111  ssenen  9121  ssfiALT  9144  domfi  9159  php  9177  domunfican  9279  mapfien  9366  ordtypelem6  9483  ordtypelem7  9484  card2inf  9515  inf3lem6  9593  cantnfle  9631  cantnflem1b  9646  cantnflem1  9649  wemapwe  9657  ttrclselem2  9686  rankxplim3  9841  fseqenlem2  9985  dfac5lem4  10086  dfac5lem4OLD  10088  dfac2b  10091  cfsuc  10217  cfflb  10219  cofsmo  10229  infpssrlem4  10266  fin4en1  10269  ssfin4  10270  fin23lem26  10285  fin23lem22  10287  fin23lem27  10288  isf34lem4  10337  isf34lem5  10338  fin1a2lem12  10371  axdc3lem2  10411  axdc4lem  10415  ttukeylem6  10474  iundom2g  10500  pwcfsdom  10543  gchen2  10586  gchor  10587  fpwwe2lem6  10596  fpwwe2lem8  10598  fpwwe2lem10  10600  fpwwe2lem11  10601  fpwwe2  10603  pwfseqlem4  10622  gchina  10659  ltexprlem6  11001  prlem936  11007  mul4  11349  2addsub  11442  muladd  11617  ltleadd  11668  leord1  11712  eqord1  11713  ltord2  11714  leord2  11715  eqord2  11716  divmul3  11849  divcan7  11898  divadddiv  11904  lemul2a  12044  lemul12b  12046  ltmuldiv2  12064  ltdivmul  12065  ledivmul  12066  ltdivmul2  12067  lt2mul2div  12068  ledivmul2  12069  lemuldiv2  12071  lt2msq  12075  ltdiv23  12081  lediv23  12082  fimaxre  12134  supadd  12158  supmullem1  12160  cju  12189  zextlt  12615  suprzcl  12621  zmax  12911  xrlttr  13107  xrre3  13138  qbtwnre  13166  xrsupsslem  13274  xrinfmsslem  13275  supxrunb1  13286  supxrunb2  13287  ixxdisj  13328  iooshf  13394  icodisj  13444  iccf1o  13464  modid  13865  modadd1  13877  modmul1  13896  seqf1o  14015  expsub  14082  sqlecan  14181  bcval5  14290  hashmap  14407  hashfacen  14426  seqcoll  14436  swrdswrdlem  14676  swrdccatin2  14701  cshwidxmod  14775  2cshwcshw  14798  cshwcshid  14800  resqreu  15225  lenegsq  15294  limsupbnd2  15456  icco1  15513  rlimresb  15538  rlimsqzlem  15622  rlimsqz  15623  rlimsqz2  15624  caucvgrlem  15646  fsum0diag2  15756  o1fsum  15786  ruclem8  16212  dvdsmulcr  16262  ndvdsadd  16387  bitsshft  16452  lcmdvds  16585  hashdvds  16752  eulerthlem2  16759  phisum  16768  pcqmul  16831  pcmpt  16870  prmreclem3  16896  4sqlem11  16933  0ram  16998  ramub1  17006  invfun  17733  initoeu2lem2  17984  coaval  18037  catcisolem  18079  funcestrcsetclem8  18115  fullestrcsetc  18119  embedsetcestrclem  18125  funcsetcestrclem8  18130  fullsetcestrc  18134  prfcl  18171  prf1st  18172  prf2nd  18173  1st2ndprf  18174  curfuncf  18206  isposd  18290  lubun  18481  isacs3lem  18508  pslem  18538  psss  18546  pwsdiagmhm  18765  grpinvid1  18930  grpinvid2  18931  grplcan  18939  grpnpncan0  18975  dfgrp3lem  18977  dfgrp3  18978  grplactcnv  18982  0nsg  19108  eqger  19117  eqg0subg  19135  qus0subgadd  19138  resghm  19171  conjghm  19188  subgga  19239  gaorber  19247  gastacl  19248  orbsta  19252  symgextf1lem  19357  psgnunilem2  19432  odid  19475  odmulg  19493  gexid  19518  odcau  19541  lsmssv  19580  lsmcom2  19592  pj1ghm  19640  frgpuptf  19707  frgpup1  19712  ghmplusg  19783  cyggex2  19834  gsumval3eu  19841  gsumval3  19844  ablfac1eu  20012  pgpfac1lem5  20018  ablsimpgfind  20049  ringurd  20101  srhmsubc  20596  isdomn4  20632  isdrngd  20681  isdrngdOLD  20683  issrngd  20771  lmhmf1o  20960  lmhmima  20961  lmhmpreima  20962  lspextmo  20970  pwssplit2  20974  pwssplit3  20975  lspdisj  21042  islbs3  21072  lbsextlem4  21078  drngnidl  21160  rngqiprngghmlem2  21205  rngqiprnglinlem1  21208  rngqiprngghm  21216  lidldvgen  21251  cnsubrg  21351  znunit  21480  cygznlem3  21486  dsmmsubg  21659  dsmmlss  21660  frlmsslsp  21712  frlmup1  21714  lindfrn  21737  f1lindf  21738  issubassa2  21808  psrbagconf1o  21845  psrgrp  21872  evlslem2  21993  mhplss  22049  psdmul  22060  psdmvr  22063  ply1sclf1  22182  mamuass  22296  dmatmul  22391  dmatsubcl  22392  dmatmulcl  22394  dmatcrng  22396  scmataddcl  22410  scmatsubcl  22411  scmatcrng  22415  mdetunilem2  22507  pm2mpf1  22693  pm2mpghm  22710  eltg2  22852  ntrss  22949  opncldf1  22978  ssnei2  23010  neindisj  23011  restopnb  23069  restntr  23076  tgcmp  23295  hauscmplem  23300  2ndc1stc  23345  2ndcdisj  23350  2ndcomap  23352  restlly  23377  lly1stc  23390  isref  23403  islocfin  23411  comppfsc  23426  txcls  23498  txdis1cn  23529  pthaus  23532  txlm  23542  qtoptop2  23593  qtopomap  23612  kqt0lem  23630  pt1hmeo  23700  ptuncnv  23701  xkocnv  23708  fbasfip  23762  fgabs  23773  fbasrn  23778  elfm2  23842  fmfnfmlem2  23849  fmfnfmlem4  23851  ptcmplem3  23948  ptcmplem4  23949  tsmsres  24038  tsmsxplem1  24047  utoptop  24129  elbl2ps  24284  elbl2  24285  blin  24316  xmeter  24328  xmetresbl  24332  stdbdxmet  24410  metrest  24419  metustexhalf  24451  dscmet  24467  nrmmetd  24469  tngngp2  24547  nmoi2  24625  icccmplem2  24719  reconnlem2  24723  metdstri  24747  metdsle  24748  metdsre  24749  metnrmlem3  24757  fsumcn  24768  icccvx  24855  bndth  24864  evth  24865  reparphti  24903  reparphtiOLD  24904  pi1blem  24946  tcphcph  25144  iscfil2  25173  cfilfcls  25181  iscau4  25186  iscauf  25187  caucfil  25190  cncmet  25229  minveclem7  25342  ovoliunlem1  25410  ovolicc2lem2  25426  ovolicc2lem3  25427  ovolicc2lem4  25428  ovolicc2lem5  25429  ovolicc2  25430  voliunlem3  25460  voliun  25462  ioombl  25473  volivth  25515  ismbfd  25547  ismbf3d  25562  itg1addlem1  25600  i1fadd  25603  itg1addlem4  25607  itg2split  25657  itg2monolem1  25658  itg2gt0  25668  ibllem  25672  itgvallem3  25694  iblposlem  25700  bddiblnc  25750  dvmptfsum  25886  rolle  25901  dvlip  25905  c1liplem1  25908  lhop1  25926  lhop2  25927  dvcvx  25932  dvfsumge  25935  dvfsumrlimge0  25944  dvfsumrlim  25945  dvfsum2  25948  mdegaddle  25986  mdegvscale  25987  mdegmullem  25990  ply1divex  26049  coeeulem  26136  plyco  26153  dgrlt  26179  vieta1  26227  ulmss  26313  ulmdvlem3  26318  iblulm  26323  tanord  26454  eff1olem  26464  logdivlt  26537  logccv  26579  lawcos  26733  xrlimcnp  26885  cxp2limlem  26893  cxp2lim  26894  cxploglim2  26896  divsqrtsumo1  26901  lgambdd  26954  sqff1o  27099  dvdsppwf1o  27103  dvdsflf1o  27104  musum  27108  muinv  27110  fsumdvdsmul  27112  fsumdvdsmulOLD  27114  sgmmul  27119  fsumvma  27131  logfac2  27135  chpchtsum  27137  logfacrlim  27142  logexprlim  27143  dchrelbas3  27156  dchrmulcl  27167  bposlem1  27202  lgsdchr  27273  lgsquadlem1  27298  lgsquadlem2  27299  lgsquad2lem2  27303  chebbnd1lem1  27387  chpchtlim  27397  rplogsumlem2  27403  dchrmusum2  27412  dchrvmasumlem1  27413  dchrvmasum2lem  27414  dchrvmasumlem2  27416  dchrvmasumlem3  27417  dchrvmasumiflem2  27420  dchrisum0flb  27428  dchrisum0fno1  27429  rpvmasum2  27430  dchrisum0re  27431  dchrisum0lem1  27434  dchrisum0lem2a  27435  dchrisum0lem2  27436  dchrisum0lem3  27437  rplogsum  27445  mulogsum  27450  mulog2sumlem2  27453  vmalogdivsum2  27456  2vmadivsumlem  27458  selberglem2  27464  selberg3lem1  27475  selberg4lem1  27478  selberg4  27479  pntrsumo1  27483  selberg34r  27489  pntrlog2bndlem1  27495  pntrlog2bndlem2  27496  pntrlog2bndlem3  27497  pntrlog2bndlem4  27498  pntrlog2bndlem5  27499  pntrlog2bndlem6  27501  pntibndlem3  27510  pntlemp  27528  ostthlem1  27545  ostth3  27556  sltres  27581  noresle  27616  nosupno  27622  nosupbday  27624  noinfno  27637  bday1s  27750  cutlt  27847  addsproplem2  27884  negsproplem2  27942  mulsuniflem  28059  mulsunif2lem  28079  precsexlem9  28124  precsexlem10  28125  precsexlem11  28126  om2noseqlt  28200  om2noseqlt2  28201  om2noseqf1o  28202  om2noseqrdg  28205  noseqrdgfn  28207  recut  28354  renegscl  28356  ercgrg  28451  oppperpex  28687  axlowdimlem15  28890  axlowdimlem16  28891  axcontlem10  28907  cusgrfilem1  29390  upgriswlk  29576  crctcshwlkn0  29758  wwlksnext  29830  wwlksnextwrd  29834  clwlkclwwlklem2a  29934  wwlksext2clwwlk  29993  grpoidinv  30444  grporcan  30454  grpoinvid1  30464  grpoinvid2  30465  grpolcan  30466  ablo4  30486  nvabs  30608  minvecolem7  30819  htthlem  30853  hvadd4  30972  hvaddsub4  31014  shscli  31253  pjspansn  31513  fh1  31554  fh2  31555  cm2j  31556  chscllem2  31574  spansncvi  31588  5oalem2  31591  5oalem5  31594  5oalem6  31595  3oalem2  31599  hoadd4  31720  cnvunop  31854  bralnfn  31884  eighmorth  31900  hmops  31956  hmopm  31957  adjlnop  32022  adjmul  32028  adjadd  32029  nmopcoi  32031  kbass5  32056  kbass6  32057  hstle  32166  stlesi  32177  mdsl0  32246  mdexchi  32271  atom1d  32289  superpos  32290  cvexchlem  32304  atomli  32318  atcvatlem  32321  chirredlem2  32327  chirredlem3  32328  atcvat4i  32333  mdsymlem1  32339  mdsymlem3  32341  mdsymlem5  32343  mdsymlem6  32344  sumdmdlem  32354  sumdmdlem2  32355  cdj1i  32369  opeldifid  32535  isoun  32632  1stpreimas  32636  f1od2  32651  indf1ofs  32796  ccatf1  32877  archirngz  33150  archiabllem1  33154  archiabllem2c  33156  qusxpid  33341  esum2d  34090  cntmeas  34223  ddemeas  34233  carsgclctunlem1  34315  itgeq12dv  34324  eulerpartlemgc  34360  eulerpartlemb  34366  eulerpartlemgs2  34378  ballotlemfc0  34491  ballotlemfcc  34492  reprss  34615  reprpmtf1o  34624  hgt750lemb  34654  bnj607  34913  derangenlem  35165  subfacp1lem3  35176  subfacp1lem5  35178  cvmliftmolem2  35276  cvmliftlem6  35284  cvmlift2lem5  35301  cvmlift2lem7  35303  cvmlift2lem9  35305  mppspstlem  35565  dfon2lem6  35783  colinbtwnle  36113  finminlem  36313  nn0prpwlem  36317  isfne  36334  neibastop1  36354  neibastop2lem  36355  neibastop3  36357  tailfb  36372  onsuct0  36436  nndivsub  36452  knoppcnlem6  36493  knoppndvlem9  36515  knoppndvlem18  36524  knoppndvlem21  36527  bj-prmoore  37110  bj-finsumval0  37280  rdgeqoa  37365  pibt2  37412  lindsadd  37614  matunitlindflem2  37618  poimirlem4  37625  poimirlem11  37632  poimirlem12  37633  poimirlem13  37634  poimirlem25  37646  poimirlem28  37649  heicant  37656  mblfinlem2  37659  mblfinlem3  37660  mblfinlem4  37661  mbfposadd  37668  itg2addnclem3  37674  ftc1anclem5  37698  ftc1anclem6  37699  ftc1anclem7  37700  ftc1anc  37702  frinfm  37736  filbcmb  37741  seqpo  37748  sstotbnd2  37775  isbndx  37783  ssbnd  37789  prdsbnd  37794  ismtycnv  37803  ismtyres  37809  heiborlem3  37814  heibor  37822  ghomdiv  37893  grpokerinj  37894  isdrngo2  37959  rngohomco  37975  rngoisocnv  37982  rngoisoco  37983  crngm4  38004  crngohomfo  38007  isidlc  38016  ispridl2  38039  ispridlc  38071  prtlem16  38869  ax12eq  38941  ax12el  38942  lshpcmp  38988  omllaw3  39245  omlfh1N  39258  cvratlem  39422  cvrat3  39443  cvrat4  39444  ps-2  39479  elpaddn0  39801  paddasslem10  39830  cdleme0cp  40215  cdleme32a  40442  cdlemeg49lebilem  40540  cdleme50eq  40542  tendoeq2  40775  diaglbN  41056  diameetN  41057  diainN  41058  dvhopN  41117  djaclN  41137  djajN  41138  dihopelvalcpre  41249  dih1dimatlem  41330  dihmeetcl  41346  djhcl  41401  mapdpglem2  41674  3factsumint1  42016  sticksstones22  42163  unitscyglem4  42193  imacrhmcl  42509  frlmsnic  42535  psrmnd  42540  evlselvlem  42581  fsuppind  42585  0prjspn  42623  infdesc  42638  ismrc  42696  eldioph2  42757  lzenom  42765  rexrabdioph  42789  fphpdo  42812  irrapxlem3  42819  elpell14qr2  42857  pell14qrreccl  42859  pell14qrdich  42864  pellfundglb  42880  monotoddzzfi  42938  2nn0ind  42941  jm2.21  42990  jm2.22  42991  dnnumch3  43043  dnwech  43044  fnwe2lem2  43047  hbtlem6  43125  cantnfresb  43320  imo72b2lem1  44165  mnuprdlem1  44268  mnuprdlem2  44269  relpmin  44949  traxext  44974  cncmpmax  45033  disjf1  45184  eliccelioc  45526  fprodexp  45599  fprodabs2  45600  mullimc  45621  mullimcf  45628  islpcn  45644  limsuppnfdlem  45706  liminfval2  45773  xlimmnfvlem1  45837  xlimmnfvlem2  45838  xlimpnfvlem1  45841  xlimpnfvlem2  45842  cncfshift  45879  cncfperiod  45884  fprodcncf  45905  dvnprodlem1  45951  dvnprodlem2  45952  stoweidlem34  46039  stoweidlem48  46053  stoweidlem60  46065  fourierdlem42  46154  fourierdlem60  46171  fourierdlem61  46172  fourierdlem63  46174  fourierdlem65  46176  fourierdlem87  46198  fourierdlem97  46208  elaa2  46239  etransclem46  46285  etransc  46288  salrestss  46366  sge0iunmptlemfi  46418  isomennd  46536  ovnsslelem  46565  ovolval4lem2  46655  smflimlem3  46778  smflimlem4  46779  smflimlem6  46781  smfpimbor1lem1  46803  smflimmpt  46815  smflimsupmpt  46834  smfliminfmpt  46837  fsetsnf1  47057  fcoresf1  47074  fvelsetpreimafv  47392  icceuelpart  47441  prproropf1olem4  47511  fmtnoprmfac2  47572  bgoldbtbndlem2  47811  bgoldbtbndlem3  47812  gpgnbgrvtx0  48069  gpgnbgrvtx1  48070  gpg3nbgrvtx0ALT  48072  gpg3nbgrvtx1  48073  srhmsubcALTV  48317  xpco2  48849  catprs  49004  uppropd  49174  thincciso2  49448  prsthinc  49457  functermc  49501  fulltermc  49504  lmdran  49664  cmdlan  49665  aacllem  49794