Theorem adantllr 717

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 483	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜑)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl1 678	1 ⊢ ((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  ad4ant13  749  ad4ant134  1174  ad5ant145  1369  oewordri  8594  marypha1lem  9430  rlimsqzlem  15597  fsumrlim  15759  fsumo1  15760  lcmdvds  16547  dfgrp3lem  18923  tgcl  22479  neindisj  22628  neiptoptop  22642  isr0  23248  cnextcn  23578  ustuqtop4  23756  mbfsup  25188  itg2i1fseqle  25279  ditgsplit  25385  itgulm  25927  leibpi  26454  dchrisumlem3  27001  legov  27874  legov2  27875  legtrid  27880  colopp  28058  f1otrg  28160  cusgrsize2inds  28748  grpoidinvlem3  29797  grpoideu  29800  grporcan  29809  blocni  30096  normcan  30867  unoplin  31211  hmoplin  31233  nmophmi  31322  mdslmd3i  31623  chirredlem1  31681  chirredlem2  31682  mdsymlem5  31698  cdj1i  31724  opreu2reuALT  31755  fpwrelmap  31996  fsumiunle  32073  ccatf1  32153  wrdt2ind  32155  archiabllem1  32380  archiabl  32385  isarchiofld  32476  ringlsmss1  32551  ringlsmss2  32552  nsgqusf1olem1  32569  nsgqusf1olem2  32570  nsgqusf1olem3  32571  rhmimaidl  32595  isprmidlc  32611  fedgmul  32775  irngnzply1  32815  locfinreflem  32889  pstmxmet  32946  ordtconnlem1  32973  esumcvg  33153  esum2d  33160  esumiun  33161  ldgenpisyslem1  33230  omssubadd  33368  signstfvneq0  33652  circlemeth  33721  mpomulcn  35231  elicc3  35288  knoppcnlem9  35463  pibt2  36384  lindsenlbs  36569  matunitlindflem1  36570  poimirlem17  36591  poimirlem20  36594  poimirlem27  36601  poimirlem29  36603  poimir  36607  heicant  36609  itg2addnclem  36625  ftc1anclem5  36651  ftc1anclem6  36652  ftc1anclem7  36653  ftc1anclem8  36654  ftc1anc  36655  fzmul  36695  fdc  36699  fdc1  36700  incsequz2  36703  rrncmslem  36786  ghomco  36845  rngoisocnv  36935  ispridlc  37024  selvvvval  41239  fsuppind  41244  cvgdvgrat  43154  binomcxplemnotnn0  43197  founiiun0  43968  supxrge  44127  suplesup  44128  supxrunb3  44188  lptre2pt  44435  0ellimcdiv  44444  limclner  44446  limsuppnfdlem  44496  limsuppnflem  44505  limsupmnflem  44515  liminfreuzlem  44597  liminflimsupclim  44602  cnrefiisplem  44624  climxlim2lem  44640  xlimliminflimsup  44657  icccncfext  44682  cncfiooiccre  44690  fperdvper  44714  dvnprodlem2  44742  iblcncfioo  44773  stoweidlem35  44830  wallispilem3  44862  fourierdlem20  44922  fourierdlem34  44936  fourierdlem39  44941  fourierdlem42  44944  fourierdlem46  44947  fourierdlem48  44949  fourierdlem49  44950  fourierdlem63  44964  fourierdlem64  44965  fourierdlem73  44974  fourierdlem87  44988  fourierdlem97  44998  fourierdlem103  45004  fourierdlem104  45005  fourierdlem111  45012  etransclem32  45061  etransclem33  45062  etransclem35  45064  sge0cl  45176  sge0f1o  45177  sge0split  45204  sge0iunmptlemre  45210  sge0rpcpnf  45216  sge0xadd  45230  nnfoctbdjlem  45250  ismeannd  45262  omeiunltfirp  45314  hoidmvlelem3  45392  hoidmvle  45395  ovncvr2  45406  hspdifhsp  45411  hspmbllem2  45422  ovnsubadd2lem  45440  pimdecfgtioo  45512  pimincfltioo  45513  smflimlem1  45566  smflimmpt  45605  smfpimne2  45635  aacllem  47926