Theorem adantrr 730

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad2antrl  741  ad2ant2r  760  ad2ant2lr  761  cases2ALT  1064  consensus  1068  3adant3  1150  3ad2antr1  1207  reusv2lem3  5369  otsndisj  5499  otiunsndisj  5500  po2nr  5580  sotric  5596  sotrieq  5597  frinf  6316  tz7.7  6414  fmptsnd  7205  fvtp1g  7234  f1cofveqaeqALT  7293  fsnex  7322  isocnv  7369  isores2  7372  isomin  7376  isoini  7377  f1oiso2  7391  ovmpodf  7608  offval  7734  ordsucun  7870  xp1st  8067  f1od2  8145  cnvf1olem  8158  fnwe2lem3  8184  fnse  8187  sexp2  8200  mpoxopoveq  8274  frrlem3  8344  frrlem13  8354  oalim  8578  omlim  8579  oaass  8607  omordi  8612  omwordri  8618  odi  8625  oen0  8633  oewordri  8639  nnawordi  8668  nnmordi  8678  omabs  8698  coflton  8718  nadd4  8746  erinxp  8850  dom2lem  9057  domssl  9063  mapen  9198  ssenen  9208  ssfiALT  9227  domfi  9242  php  9260  fissorduni  9320  domunfican  9351  mapfien  9437  ordtypelem6  9554  ordtypelem7  9555  card2inf  9586  inf3lem6  9671  cantnfle  9709  cantnflem1b  9724  cantnflem1  9727  wemapwe  9735  ttrclselem2  9764  rankxplim3  9935  fseqenlem2  10143  dfac5lem4  10244  dfac2b  10248  cfsuc  10374  cfflb  10376  cofsmo  10386  infpssrlem4  10423  fin4en1  10426  ssfin4  10427  fin23lem26  10442  fin23lem22  10444  fin23lem27  10445  isf34lem4  10494  isf34lem5  10495  fin1a2lem12  10528  axdc3lem2  10568  axdc4lem  10572  ttukeylem6  10631  iundom2g  10663  pwcfsdom  10707  gchen2  10750  gchor  10751  fpwwe2lem6  10760  fpwwe2lem8  10762  fpwwe2lem10  10764  fpwwe2lem11  10765  fpwwe2  10767  pwfseqlem4  10786  gchina  10823  ltexprlem6  11165  prlem936  11171  mul4  11517  2addsub  11610  muladd  11787  ltleadd  11839  leord1  11883  eqord1  11884  ltord2  11885  leord2  11886  eqord2  11887  divmul3  12019  divcan7  12066  divadddiv  12072  lemul2a  12212  lemul12b  12214  ltmuldiv2  12231  ltdivmul  12232  ledivmul  12233  ltdivmul2  12234  lt2mul2div  12235  ledivmul2  12236  lemuldiv2  12238  lt2msq  12242  ltdiv23  12248  lediv23  12249  fimaxre  12301  supadd  12325  supmullem1  12327  cju  12356  zextlt  12813  suprzcl  12819  zmax  13112  xrlttr  13309  xrre3  13341  qbtwnre  13369  xrsupsslem  13477  xrinfmsslem  13478  supxrunb1  13489  supxrunb2  13490  ixxdisj  13531  iooshf  13597  icodisj  13647  iccf1o  13667  modid  14076  modadd1  14088  modmul1  14107  seqf1o  14226  expsub  14293  sqlecan  14393  bcval5  14503  hashmap  14621  hashfacen  14640  seqcoll  14650  ccatf1  14777  swrdswrdlem  14895  swrdccatin2  14920  cshwidxmod  14996  2cshwcshw  15018  cshwcshid  15020  resqreu  15462  lenegsq  15531  limsupbnd2  15694  icco1  15751  rlimresb  15776  rlimsqzlem  15860  rlimsqz  15861  rlimsqz2  15862  caucvgrlem  15884  fsum0diag2  15993  o1fsum  16024  ruclem8  16449  dvdsmulcr  16499  ndvdsadd  16624  bitsshft  16689  lcmdvds  16827  hashdvds  16996  eulerthlem2  17003  phisum  17012  pcqmul  17075  pcmpt  17114  prmreclem3  17140  4sqlem11  17177  0ram  17242  ramub1  17250  invfun  17989  initoeu2lem2  18240  coaval  18293  catcisolem  18335  funcestrcsetclem8  18371  fullestrcsetc  18375  embedsetcestrclem  18381  funcsetcestrclem8  18386  fullsetcestrc  18390  prfcl  18427  prf1st  18428  prf2nd  18429  1st2ndprf  18430  curfuncf  18462  isposd  18546  lubun  18739  isacs3lem  18766  pslem  18796  psss  18804  chnccat  18850  chnpof1  18854  pwsdiagmhm  19077  grpinvid1  19252  grpinvid2  19253  grplcan  19261  grpnpncan0  19296  dfgrp3lem  19298  dfgrp3  19299  grplactcnv  19303  0nsg  19429  eqger  19440  qusxpid  19445  eqg0subg  19461  qus0subgadd  19464  resghm  19496  conjghm  19513  subgga  19565  gaorber  19573  gastacl  19574  orbsta  19578  symgextf1lem  19685  psgnunilem2  19760  odid  19803  odmulg  19821  gexid  19846  odcau  19869  lsmssv  19908  lsmcom2  19920  pj1ghm  19968  frgpuptf  20035  frgpup1  20040  ghmplusg  20111  cyggex2  20162  gsumval3eu  20169  gsumval3  20172  ablfac1eu  20340  pgpfac1lem5  20346  ablsimpgfind  20377  ringurd  20462  srhmsubc  20983  isdomn4  21018  isdrngd  21073  isdrngdOLD  21075  issrngd  21163  lmhmf1o  21372  lmhmima  21373  lmhmpreima  21374  lspextmo  21382  pwssplit2  21386  pwssplit3  21387  lspdisj  21454  islbs3  21484  lbsextlem4  21490  drngnidl  21582  rngqiprngghmlem2  21635  rngqiprnglinlem1  21638  rngqiprngghm  21646  lidldvgen  21709  cnsubrg  21787  znunit  21924  cygznlem3  21930  dsmmsubg  22104  dsmmlss  22105  frlmsslsp  22157  frlmup1  22159  lindfrn  22182  f1lindf  22183  issubassa2  22255  psrbagconf1o  22292  psrgrp  22319  evlslem2  22443  mhplss  22531  psdmul  22542  psdmvr  22545  ply1sclf1  22663  mamuass  22772  dmatmul  22867  dmatsubcl  22868  dmatmulcl  22870  dmatcrng  22872  scmataddcl  22886  scmatsubcl  22887  scmatcrng  22891  mdetunilem2  22983  matunitlindflem2  23050  pm2mpf1  23172  pm2mpghm  23189  eltg2  23331  ntrss  23428  opncldf1  23457  ssnei2  23489  neindisj  23490  restopnb  23548  restntr  23555  tgcmp  23774  hauscmplem  23779  2ndc1stc  23824  2ndcdisj  23830  2ndcomap  23832  restlly  23857  lly1stc  23870  isref  23883  islocfin  23891  comppfsc  23906  txcls  23978  txdis1cn  24009  pthaus  24012  txlm  24022  qtoptop2  24073  qtopomap  24092  kqt0lem  24110  pt1hmeo  24180  ptuncnv  24181  xkocnv  24188  fbasfip  24242  fgabs  24253  fbasrn  24258  elfm2  24322  fmfnfmlem2  24329  fmfnfmlem4  24331  ptcmplem3  24428  ptcmplem4  24429  tsmsres  24518  tsmsxplem1  24527  utoptop  24608  elbl2ps  24763  elbl2  24764  blin  24795  xmeter  24807  xmetresbl  24811  stdbdxmet  24889  metrest  24898  metustexhalf  24930  dscmet  24946  nrmmetd  24948  tngngp2  25026  nmoi2  25104  icccmplem2  25198  reconnlem2  25202  metdstri  25226  metdsle  25227  metdsre  25228  metnrmlem3  25236  fsumcn  25246  icccvx  25326  bndth  25334  evth  25335  reparphti  25373  pi1blem  25415  tcphcph  25613  iscfil2  25642  cfilfcls  25650  iscau4  25655  iscauf  25656  caucfil  25659  cncmet  25698  minveclem7  25811  ovoliunlem1  25878  ovolicc2lem2  25894  ovolicc2lem3  25895  ovolicc2lem4  25896  ovolicc2lem5  25897  ovolicc2  25898  voliunlem3  25928  voliun  25930  ioombl  25941  volivth  25983  ismbfd  26015  ismbf3d  26030  itg1addlem1  26068  i1fadd  26071  itg1addlem4  26075  itg2split  26125  itg2monolem1  26126  itg2gt0  26136  ibllem  26140  itgvallem3  26161  iblposlem  26167  bddiblnc  26217  dvmptfsum  26350  rolle  26365  dvlip  26368  c1liplem1  26371  lhop1  26389  lhop2  26390  dvcvx  26395  dvfsumge  26397  dvfsumrlimge0  26405  dvfsumrlim  26406  dvfsum2  26409  mdegaddle  26447  mdegvscale  26448  mdegmullem  26451  ply1divex  26510  coeeulem  26598  plyco  26615  dgrlt  26640  vieta1  26690  ulmss  26781  ulmdvlem3  26786  iblulm  26791  tanord  26923  eff1olem  26933  logdivlt  27006  logccv  27048  lawcos  27201  xrlimcnp  27353  cxp2limlem  27360  cxp2lim  27361  cxploglim2  27363  divsqrtsumo1  27368  lgambdd  27421  sqff1o  27566  dvdsppwf1o  27570  dvdsflf1o  27571  musum  27575  muinv  27577  fsumdvdsmul  27579  sgmmul  27585  fsumvma  27597  logfac2  27601  chpchtsum  27603  logfacrlim  27608  logexprlim  27609  dchrelbas3  27622  dchrmulcl  27633  bposlem1  27668  lgsdchr  27739  lgsquadlem1  27764  lgsquadlem2  27765  lgsquad2lem2  27769  chebbnd1lem1  27853  chpchtlim  27863  rplogsumlem2  27869  dchrmusum2  27878  dchrvmasumlem1  27879  dchrvmasum2lem  27880  dchrvmasumlem2  27882  dchrvmasumlem3  27883  dchrvmasumiflem2  27886  dchrisum0flb  27894  dchrisum0fno1  27895  rpvmasum2  27896  dchrisum0re  27897  dchrisum0lem1  27900  dchrisum0lem2a  27901  dchrisum0lem2  27902  dchrisum0lem3  27903  rplogsum  27911  mulogsum  27916  mulog2sumlem2  27919  vmalogdivsum2  27922  2vmadivsumlem  27924  selberglem2  27930  selberg3lem1  27941  selberg4lem1  27944  selberg4  27945  pntrsumo1  27949  selberg34r  27955  pntrlog2bndlem1  27961  pntrlog2bndlem2  27962  pntrlog2bndlem3  27963  pntrlog2bndlem4  27964  pntrlog2bndlem5  27965  pntrlog2bndlem6  27967  pntibndlem3  27976  pntlemp  27994  ostthlem1  28011  ostth3  28022  infdesc  28024  ltsres  28076  noresle  28111  nosupno  28117  nosupbday  28119  noinfno  28132  bday1  28257  cutlt  28375  addsproplem2  28413  negsproplem2  28472  mulsuniflem  28592  mulsunif2lem  28612  precsexlem9  28658  precsexlem10  28659  precsexlem11  28660  om2noseqlt  28742  om2noseqlt2  28743  om2noseqf1o  28744  om2noseqrdg  28747  noseqrdgfn  28749  bdaypw2n0bndlem  28906  bdayfinbndlem1  28910  recut  28937  elreno2  28938  renegscl  28941  ercgrg  29037  oppperpex  29286  axlowdimlem15  29591  axlowdimlem16  29592  axcontlem10  29608  cusgrfilem1  30093  upgriswlk  30278  crctcshwlkn0  30467  wwlksnext  30539  wwlksnextwrd  30543  clwlkclwwlklem2a  30646  wwlksext2clwwlk  30705  grpoidinv  31167  grporcan  31177  grpoinvid1  31187  grpoinvid2  31188  grpolcan  31189  ablo4  31209  nvabs  31331  minvecolem7  31542  htthlem  31576  hvadd4  31695  hvaddsub4  31737  shscli  31976  pjspansn  32236  fh1  32277  fh2  32278  cm2j  32279  chscllem2  32297  spansncvi  32311  5oalem2  32314  5oalem5  32317  5oalem6  32318  3oalem2  32322  hoadd4  32443  cnvunop  32577  bralnfn  32607  eighmorth  32623  hmops  32679  hmopm  32680  adjlnop  32745  adjmul  32751  adjadd  32752  nmopcoi  32754  kbass5  32779  kbass6  32780  hstle  32889  stlesi  32900  mdsl0  32969  mdexchi  32994  atom1d  33012  superpos  33013  cvexchlem  33027  atomli  33041  atcvatlem  33044  chirredlem2  33050  chirredlem3  33051  atcvat4i  33056  mdsymlem1  33062  mdsymlem3  33064  mdsymlem5  33066  mdsymlem6  33067  sumdmdlem  33077  sumdmdlem2  33078  cdj1i  33092  opeldifid  33291  isoun  33392  1stpreimas  33396  indf1ofs  33529  weinflb  33637  archirngz  33849  archiabllem1  33853  archiabllem2c  33855  esum2d  34836  cntmeas  34970  ddemeas  34980  carsgclctunlem1  35060  itgeq12dv  35069  eulerpartlemgc  35105  eulerpartlemb  35111  eulerpartlemgs2  35123  ballotlemfc0  35236  ballotlemfcc  35237  reprss  35357  reprpmtf1o  35366  hgt750lemb  35396  bnj607  35657  brlexod  36040  brr0d  36042  derangenlem  36144  subfacp1lem3  36155  subfacp1lem5  36157  cvmliftmolem2  36255  cvmliftlem6  36263  cvmlift2lem5  36280  cvmlift2lem7  36282  cvmlift2lem9  36284  mppspstlem  36544  dfon2lem6  36765  colinbtwnle  37098  nmulrid  37161  ltnadd  37182  nadddilem2  37185  nadddilem4  37187  finminlem  37321  nn0prpwlem  37325  isfne  37342  neibastop1  37362  neibastop2lem  37363  neibastop3  37365  tailfb  37380  onsuct0  37444  nndivsub  37460  knoppcnlem6  37579  knoppndvlem9  37601  knoppndvlem18  37610  knoppndvlem21  37613  bj-prmoore  38306  bj-finsumval0  38474  rdgeqoa  38561  pibt2  38608  lindsadd  38804  poimirlem4  38810  poimirlem11  38817  poimirlem12  38818  poimirlem13  38819  poimirlem25  38831  poimirlem28  38834  heicant  38841  mblfinlem2  38844  mblfinlem3  38845  mblfinlem4  38846  mbfposadd  38853  itg2addnclem3  38859  ftc1anclem5  38883  ftc1anclem6  38884  ftc1anclem7  38885  ftc1anc  38887  filbcmb  38940  seqpo  38947  sstotbnd2  38974  isbndx  38982  ssbnd  38988  prdsbnd  38993  ismtycnv  39002  ismtyres  39008  heiborlem3  39013  heibor  39021  ghomdiv  39092  grpokerinj  39093  isdrngo2  39158  rngohomco  39174  rngoisocnv  39181  rngoisoco  39182  crngm4  39203  crngohomfo  39206  isidlc  39215  ispridl2  39238  ispridlc  39270  prtlem16  40192  ax12eq  40264  ax12el  40265  lshpcmp  40311  omllaw3  40568  omlfh1N  40581  cvratlem  40744  cvrat3  40765  cvrat4  40766  ps-2  40801  elpaddn0  41123  paddasslem10  41152  cdleme0cp  41537  cdleme32a  41764  cdlemeg49lebilem  41862  cdleme50eq  41864  tendoeq2  42097  diaglbN  42378  diameetN  42379  diainN  42380  dvhopN  42439  djaclN  42459  djajN  42460  dihopelvalcpre  42571  dih1dimatlem  42652  dihmeetcl  42668  djhcl  42723  mapdpglem2  42996  3factsumint1  43337  sticksstones22  43484  unitscyglem4  43514  imacrhmcl  43847  frlmsnic  43870  psrmnd  43873  evlselvlem  43882  fsuppind  43884  0prjspn  43930  ismrc  43978  eldioph2  44039  lzenom  44047  rexrabdioph  44067  fphpdo  44090  irrapxlem3  44097  elpell14qr2  44135  pell14qrreccl  44137  pell14qrdich  44142  pellfundglb  44158  monotoddzzfi  44215  2nn0ind  44218  jm2.21  44267  jm2.22  44268  dnnumch3  44320  dnwech  44321  hbtlem6  44396  cantnfresb  44587  imo72b2lem1  45430  mnuprdlem1  45517  mnuprdlem2  45518  relpmin  46206  traxext  46231  cncmpmax  46323  disjf1  46471  eliccelioc  46806  fprodexp  46879  fprodabs2  46880  mullimc  46901  mullimcf  46908  islpcn  46922  limsuppnfdlem  46984  liminfval2  47051  xlimmnfvlem1  47115  xlimmnfvlem2  47116  xlimpnfvlem1  47119  xlimpnfvlem2  47120  cncfshift  47157  cncfperiod  47162  fprodcncf  47183  dvnprodlem1  47229  dvnprodlem2  47230  stoweidlem34  47317  stoweidlem48  47331  stoweidlem60  47343  fourierdlem42  47432  fourierdlem60  47449  fourierdlem61  47450  fourierdlem63  47452  fourierdlem65  47454  fourierdlem87  47476  fourierdlem97  47486  elaa2  47517  etransclem46  47563  etransc  47566  salrestss  47644  sge0iunmptlemfi  47696  isomennd  47814  ovnsslelem  47843  ovolval4lem2  47933  smflimlem3  48056  smflimlem4  48057  smflimlem6  48059  smfpimbor1lem1  48081  smflimmpt  48093  smflimsupmpt  48112  smfliminfmpt  48115  fsetsnf1  48395  fcoresf1  48412  fvelsetpreimafv  48742  icceuelpart  48791  prproropf1olem4  48861  fmtnoprmfac2  48925  bgoldbtbndlem2  49177  bgoldbtbndlem3  49178  gpgnbgrvtx0  49445  gpgnbgrvtx1  49446  gpg3nbgrvtx0ALT  49448  gpg3nbgrvtx1  49449  srhmsubcALTV  49695  xpco2  50299  catprs  50456  uppropd  50628  thincciso2  50921  prsthinc  50930  functermc  50974  fulltermc  50977  lmdran  51185  cmdlan  51186  aacllem  51367