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  1397  oewordri  8632  marypha1lem  9455  ccatf1  14766  rlimsqzlem  15848  fsumrlim  16010  fsumo1  16011  lcmdvds  16815  chnind  18827  dfgrp3lem  19280  isprmidlc  21661  lindsenlbs  22190  selvvvval  22484  matunitlindflem1  23027  tgcl  23320  neindisj  23468  neiptoptop  23482  isr0  24089  cnextcn  24419  ustuqtop4  24596  mpomulcn  25221  mbfsup  26018  itg2i1fseqle  26108  ditgsplit  26214  itgulm  26768  leibpi  27303  dchrisumlem3  27851  legov  29081  legov2  29082  legtrid  29087  colopp  29280  perpprlng  29461  f1otrg  29481  cusgrsize2inds  30067  grpoidinvlem3  31141  grpoideu  31144  grporcan  31153  blocni  31440  normcan  32211  unoplin  32555  hmoplin  32577  nmophmi  32666  mdslmd3i  32967  chirredlem1  33025  chirredlem2  33026  mdsymlem5  33042  cdj1i  33068  opreu2reuALT  33148  fpwrelmap  33398  fsumiunle  33493  wrdt2ind  33589  suppgsumssiun  33709  gsumwrd2dccatlem  33714  archiabllem1  33830  archiabl  33835  isarchiofld  33836  elrgspnlem1  33879  elrgspnlem2  33880  elrgspnlem4  33882  elrgspnsubrunlem2  33885  ringlsmss1  34033  ringlsmss2  34034  nsgqusf1olem1  34048  nsgqusf1olem2  34049  nsgqusf1olem3  34050  rhmimaidl  34066  mplvrpmrhm  34262  esplyfv1  34284  esplyfval1  34288  fedgmul  34346  irngnzply1  34406  locfinreflem  34555  pstmxmet  34612  ordtconnlem1  34639  esumcvg  34801  esum2d  34808  esumiun  34809  ldgenpisyslem1  34879  omssubadd  35015  signstfvneq0  35284  circlemeth  35352  elicc3  37296  knoppcnlem9  37558  pibt2  38545  poimirlem17  38760  poimirlem20  38763  poimirlem27  38770  poimirlem29  38772  poimir  38776  heicant  38778  itg2addnclem  38794  ftc1anclem5  38820  ftc1anclem6  38821  ftc1anclem7  38822  ftc1anclem8  38823  ftc1anc  38824  fzmul  38878  fdc  38882  fdc1  38883  incsequz2  38886  rrncmslem  38969  ghomco  39028  rngoisocnv  39118  ispridlc  39207  fiabv  43804  fsuppind  43822  cvgdvgrat  45500  binomcxplemnotnn0  45543  founiiun0  46420  supxrge  46565  suplesup  46566  supxrunb3  46625  lptre2pt  46865  0ellimcdiv  46874  limclner  46876  limsuppnfdlem  46926  limsuppnflem  46935  limsupmnflem  46945  liminfreuzlem  47027  liminflimsupclim  47032  cnrefiisplem  47054  climxlim2lem  47070  xlimliminflimsup  47087  icccncfext  47112  cncfiooiccre  47120  fperdvper  47144  dvnprodlem2  47172  iblcncfioo  47203  stoweidlem35  47260  wallispilem3  47292  fourierdlem20  47352  fourierdlem34  47366  fourierdlem39  47371  fourierdlem42  47374  fourierdlem46  47377  fourierdlem48  47379  fourierdlem49  47380  fourierdlem63  47394  fourierdlem64  47395  fourierdlem73  47404  fourierdlem87  47418  fourierdlem97  47428  fourierdlem103  47434  fourierdlem104  47435  fourierdlem111  47442  etransclem32  47491  etransclem33  47492  etransclem35  47494  sge0cl  47606  sge0f1o  47607  sge0split  47634  sge0iunmptlemre  47640  sge0rpcpnf  47646  sge0xadd  47660  nnfoctbdjlem  47680  ismeannd  47692  omeiunltfirp  47744  hoidmvlelem3  47822  hoidmvle  47825  ovncvr2  47836  hspdifhsp  47841  hspmbllem2  47852  ovnsubadd2lem  47870  pimdecfgtioo  47942  pimincfltioo  47943  smflimlem1  47996  smflimmpt  48035  smfpimne2  48065  resccat  50403  aacllem  51251