Theorem adantllr 732

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 488	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜑)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl1 693	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:  ad4ant13  764  ad4ant134  1193  ad5ant145  1396  oewordri  8601  marypha1lem  9425  ccatf1  14736  rlimsqzlem  15816  fsumrlim  15978  fsumo1  15979  lcmdvds  16783  chnind  18795  dfgrp3lem  19248  isprmidlc  21628  lindsenlbs  22157  selvvvval  22451  matunitlindflem1  22994  tgcl  23287  neindisj  23435  neiptoptop  23449  isr0  24056  cnextcn  24386  ustuqtop4  24563  mpomulcn  25188  mbfsup  25985  itg2i1fseqle  26075  ditgsplit  26181  itgulm  26735  leibpi  27270  dchrisumlem3  27818  legov  29048  legov2  29049  legtrid  29054  colopp  29247  perpprlng  29428  f1otrg  29448  cusgrsize2inds  30034  grpoidinvlem3  31108  grpoideu  31111  grporcan  31120  blocni  31407  normcan  32178  unoplin  32522  hmoplin  32544  nmophmi  32633  mdslmd3i  32934  chirredlem1  32992  chirredlem2  32993  mdsymlem5  33009  cdj1i  33035  opreu2reuALT  33073  fpwrelmap  33325  fsumiunle  33420  wrdt2ind  33516  suppgsumssiun  33633  gsumwrd2dccatlem  33638  archiabllem1  33754  archiabl  33759  isarchiofld  33760  elrgspnlem1  33803  elrgspnlem2  33804  elrgspnlem4  33806  elrgspnsubrunlem2  33809  ringlsmss1  33949  ringlsmss2  33950  nsgqusf1olem1  33964  nsgqusf1olem2  33965  nsgqusf1olem3  33966  rhmimaidl  33982  mplvrpmrhm  34179  esplyfv1  34201  esplyfval1  34205  fedgmul  34263  irngnzply1  34323  locfinreflem  34472  pstmxmet  34529  ordtconnlem1  34556  esumcvg  34718  esum2d  34725  esumiun  34726  ldgenpisyslem1  34796  omssubadd  34932  signstfvneq0  35201  circlemeth  35269  elicc3  37105  knoppcnlem9  37367  pibt2  38341  poimirlem17  38556  poimirlem20  38559  poimirlem27  38566  poimirlem29  38568  poimir  38572  heicant  38574  itg2addnclem  38590  ftc1anclem5  38616  ftc1anclem6  38617  ftc1anclem7  38618  ftc1anclem8  38619  ftc1anc  38620  fzmul  38676  fdc  38680  fdc1  38681  incsequz2  38684  rrncmslem  38767  ghomco  38826  rngoisocnv  38916  ispridlc  39005  fiabv  43601  fsuppind  43619  cvgdvgrat  45297  binomcxplemnotnn0  45340  founiiun0  46205  supxrge  46350  suplesup  46351  supxrunb3  46410  lptre2pt  46650  0ellimcdiv  46659  limclner  46661  limsuppnfdlem  46711  limsuppnflem  46720  limsupmnflem  46730  liminfreuzlem  46812  liminflimsupclim  46817  cnrefiisplem  46839  climxlim2lem  46855  xlimliminflimsup  46872  icccncfext  46897  cncfiooiccre  46905  fperdvper  46929  dvnprodlem2  46957  iblcncfioo  46988  stoweidlem35  47045  wallispilem3  47077  fourierdlem20  47137  fourierdlem34  47151  fourierdlem39  47156  fourierdlem42  47159  fourierdlem46  47162  fourierdlem48  47164  fourierdlem49  47165  fourierdlem63  47179  fourierdlem64  47180  fourierdlem73  47189  fourierdlem87  47203  fourierdlem97  47213  fourierdlem103  47219  fourierdlem104  47220  fourierdlem111  47227  etransclem32  47276  etransclem33  47277  etransclem35  47279  sge0cl  47391  sge0f1o  47392  sge0split  47419  sge0iunmptlemre  47425  sge0rpcpnf  47431  sge0xadd  47445  nnfoctbdjlem  47465  ismeannd  47477  omeiunltfirp  47529  hoidmvlelem3  47607  hoidmvle  47610  ovncvr2  47621  hspdifhsp  47626  hspmbllem2  47637  ovnsubadd2lem  47655  pimdecfgtioo  47727  pimincfltioo  47728  smflimlem1  47781  smflimmpt  47820  smfpimne2  47850  resccat  50182  aacllem  50939