Theorem adantllr 719

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 680	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 207  df-an 396

This theorem is referenced by:  ad4ant13  751  ad4ant134  1175  ad5ant145  1371  oewordri  8507  marypha1lem  9317  rlimsqzlem  15556  fsumrlim  15718  fsumo1  15719  lcmdvds  16519  chnind  18527  dfgrp3lem  18951  tgcl  22885  neindisj  23033  neiptoptop  23047  isr0  23653  cnextcn  23983  ustuqtop4  24160  mpomulcn  24786  mbfsup  25593  itg2i1fseqle  25683  ditgsplit  25790  itgulm  26345  leibpi  26880  dchrisumlem3  27430  legov  28564  legov2  28565  legtrid  28570  colopp  28748  f1otrg  28850  cusgrsize2inds  29433  grpoidinvlem3  30484  grpoideu  30487  grporcan  30496  blocni  30783  normcan  31554  unoplin  31898  hmoplin  31920  nmophmi  32009  mdslmd3i  32310  chirredlem1  32368  chirredlem2  32369  mdsymlem5  32385  cdj1i  32411  opreu2reuALT  32454  fpwrelmap  32714  fsumiunle  32810  ccatf1  32928  wrdt2ind  32932  gsumwrd2dccatlem  33044  archiabllem1  33160  archiabl  33165  isarchiofld  33166  elrgspnlem1  33207  elrgspnlem2  33208  elrgspnlem4  33210  elrgspnsubrunlem2  33213  ringlsmss1  33359  ringlsmss2  33360  nsgqusf1olem1  33376  nsgqusf1olem2  33377  nsgqusf1olem3  33378  rhmimaidl  33395  isprmidlc  33410  mplvrpmrhm  33575  esplyfv1  33588  fedgmul  33642  irngnzply1  33702  locfinreflem  33851  pstmxmet  33908  ordtconnlem1  33935  esumcvg  34097  esum2d  34104  esumiun  34105  ldgenpisyslem1  34174  omssubadd  34311  signstfvneq0  34583  circlemeth  34651  elicc3  36357  knoppcnlem9  36541  pibt2  37457  lindsenlbs  37661  matunitlindflem1  37662  poimirlem17  37683  poimirlem20  37686  poimirlem27  37693  poimirlem29  37695  poimir  37699  heicant  37701  itg2addnclem  37717  ftc1anclem5  37743  ftc1anclem6  37744  ftc1anclem7  37745  ftc1anclem8  37746  ftc1anc  37747  fzmul  37787  fdc  37791  fdc1  37792  incsequz2  37795  rrncmslem  37878  ghomco  37937  rngoisocnv  38027  ispridlc  38116  fiabv  42575  selvvvval  42624  fsuppind  42629  cvgdvgrat  44352  binomcxplemnotnn0  44395  founiiun0  45233  supxrge  45383  suplesup  45384  supxrunb3  45443  lptre2pt  45684  0ellimcdiv  45693  limclner  45695  limsuppnfdlem  45745  limsuppnflem  45754  limsupmnflem  45764  liminfreuzlem  45846  liminflimsupclim  45851  cnrefiisplem  45873  climxlim2lem  45889  xlimliminflimsup  45906  icccncfext  45931  cncfiooiccre  45939  fperdvper  45963  dvnprodlem2  45991  iblcncfioo  46022  stoweidlem35  46079  wallispilem3  46111  fourierdlem20  46171  fourierdlem34  46185  fourierdlem39  46190  fourierdlem42  46193  fourierdlem46  46196  fourierdlem48  46198  fourierdlem49  46199  fourierdlem63  46213  fourierdlem64  46214  fourierdlem73  46223  fourierdlem87  46237  fourierdlem97  46247  fourierdlem103  46253  fourierdlem104  46254  fourierdlem111  46261  etransclem32  46310  etransclem33  46311  etransclem35  46313  sge0cl  46425  sge0f1o  46426  sge0split  46453  sge0iunmptlemre  46459  sge0rpcpnf  46465  sge0xadd  46479  nnfoctbdjlem  46499  ismeannd  46511  omeiunltfirp  46563  hoidmvlelem3  46641  hoidmvle  46644  ovncvr2  46655  hspdifhsp  46660  hspmbllem2  46671  ovnsubadd2lem  46689  pimdecfgtioo  46761  pimincfltioo  46762  smflimlem1  46815  smflimmpt  46854  smfpimne2  46884  resccat  49112  aacllem  49839