Theorem adantllr 716

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)

Hypothesis

Ref	Expression
adantl2.1	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
adantllr	⊢ ((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem adantllr

Step	Hyp	Ref	Expression
1		simpl 482	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜑)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl1 677	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 206  df-an 396

This theorem is referenced by:  ad4ant13  748  ad4ant134  1173  ad5ant145  1368  oewordri  8598  marypha1lem  9434  rlimsqzlem  15602  fsumrlim  15764  fsumo1  15765  lcmdvds  16552  dfgrp3lem  18961  tgcl  22705  neindisj  22854  neiptoptop  22868  isr0  23474  cnextcn  23804  ustuqtop4  23982  mpomulcn  24618  mbfsup  25426  itg2i1fseqle  25517  ditgsplit  25623  itgulm  26170  leibpi  26698  dchrisumlem3  27245  legov  28118  legov2  28119  legtrid  28124  colopp  28302  f1otrg  28404  cusgrsize2inds  28992  grpoidinvlem3  30041  grpoideu  30044  grporcan  30053  blocni  30340  normcan  31111  unoplin  31455  hmoplin  31477  nmophmi  31566  mdslmd3i  31867  chirredlem1  31925  chirredlem2  31926  mdsymlem5  31942  cdj1i  31968  opreu2reuALT  31999  fpwrelmap  32240  fsumiunle  32317  ccatf1  32397  wrdt2ind  32399  archiabllem1  32624  archiabl  32629  isarchiofld  32720  ringlsmss1  32795  ringlsmss2  32796  nsgqusf1olem1  32813  nsgqusf1olem2  32814  nsgqusf1olem3  32815  rhmimaidl  32839  isprmidlc  32855  fedgmul  33019  irngnzply1  33059  locfinreflem  33133  pstmxmet  33190  ordtconnlem1  33217  esumcvg  33397  esum2d  33404  esumiun  33405  ldgenpisyslem1  33474  omssubadd  33612  signstfvneq0  33896  circlemeth  33965  elicc3  35518  knoppcnlem9  35693  pibt2  36614  lindsenlbs  36799  matunitlindflem1  36800  poimirlem17  36821  poimirlem20  36824  poimirlem27  36831  poimirlem29  36833  poimir  36837  heicant  36839  itg2addnclem  36855  ftc1anclem5  36881  ftc1anclem6  36882  ftc1anclem7  36883  ftc1anclem8  36884  ftc1anc  36885  fzmul  36925  fdc  36929  fdc1  36930  incsequz2  36933  rrncmslem  37016  ghomco  37075  rngoisocnv  37165  ispridlc  37254  selvvvval  41472  fsuppind  41477  cvgdvgrat  43387  binomcxplemnotnn0  43430  founiiun0  44200  supxrge  44359  suplesup  44360  supxrunb3  44420  lptre2pt  44667  0ellimcdiv  44676  limclner  44678  limsuppnfdlem  44728  limsuppnflem  44737  limsupmnflem  44747  liminfreuzlem  44829  liminflimsupclim  44834  cnrefiisplem  44856  climxlim2lem  44872  xlimliminflimsup  44889  icccncfext  44914  cncfiooiccre  44922  fperdvper  44946  dvnprodlem2  44974  iblcncfioo  45005  stoweidlem35  45062  wallispilem3  45094  fourierdlem20  45154  fourierdlem34  45168  fourierdlem39  45173  fourierdlem42  45176  fourierdlem46  45179  fourierdlem48  45181  fourierdlem49  45182  fourierdlem63  45196  fourierdlem64  45197  fourierdlem73  45206  fourierdlem87  45220  fourierdlem97  45230  fourierdlem103  45236  fourierdlem104  45237  fourierdlem111  45244  etransclem32  45293  etransclem33  45294  etransclem35  45296  sge0cl  45408  sge0f1o  45409  sge0split  45436  sge0iunmptlemre  45442  sge0rpcpnf  45448  sge0xadd  45462  nnfoctbdjlem  45482  ismeannd  45494  omeiunltfirp  45546  hoidmvlelem3  45624  hoidmvle  45627  ovncvr2  45638  hspdifhsp  45643  hspmbllem2  45654  ovnsubadd2lem  45672  pimdecfgtioo  45744  pimincfltioo  45745  smflimlem1  45798  smflimmpt  45837  smfpimne2  45867  aacllem  47948