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  8517  marypha1lem  9342  rlimsqzlem  15574  fsumrlim  15736  fsumo1  15737  lcmdvds  16537  dfgrp3lem  18935  tgcl  22872  neindisj  23020  neiptoptop  23034  isr0  23640  cnextcn  23970  ustuqtop4  24148  mpomulcn  24774  mbfsup  25581  itg2i1fseqle  25671  ditgsplit  25778  itgulm  26333  leibpi  26868  dchrisumlem3  27418  legov  28548  legov2  28549  legtrid  28554  colopp  28732  f1otrg  28834  cusgrsize2inds  29417  grpoidinvlem3  30468  grpoideu  30471  grporcan  30480  blocni  30767  normcan  31538  unoplin  31882  hmoplin  31904  nmophmi  31993  mdslmd3i  32294  chirredlem1  32352  chirredlem2  32353  mdsymlem5  32369  cdj1i  32395  opreu2reuALT  32439  fpwrelmap  32689  fsumiunle  32787  ccatf1  32903  wrdt2ind  32908  chnind  32966  gsumwrd2dccatlem  33032  archiabllem1  33148  archiabl  33153  isarchiofld  33154  elrgspnlem1  33195  elrgspnlem2  33196  elrgspnlem4  33198  elrgspnsubrunlem2  33201  ringlsmss1  33346  ringlsmss2  33347  nsgqusf1olem1  33363  nsgqusf1olem2  33364  nsgqusf1olem3  33365  rhmimaidl  33382  isprmidlc  33397  fedgmul  33606  irngnzply1  33665  locfinreflem  33809  pstmxmet  33866  ordtconnlem1  33893  esumcvg  34055  esum2d  34062  esumiun  34063  ldgenpisyslem1  34132  omssubadd  34270  signstfvneq0  34542  circlemeth  34610  elicc3  36293  knoppcnlem9  36477  pibt2  37393  lindsenlbs  37597  matunitlindflem1  37598  poimirlem17  37619  poimirlem20  37622  poimirlem27  37629  poimirlem29  37631  poimir  37635  heicant  37637  itg2addnclem  37653  ftc1anclem5  37679  ftc1anclem6  37680  ftc1anclem7  37681  ftc1anclem8  37682  ftc1anc  37683  fzmul  37723  fdc  37727  fdc1  37728  incsequz2  37731  rrncmslem  37814  ghomco  37873  rngoisocnv  37963  ispridlc  38052  fiabv  42512  selvvvval  42561  fsuppind  42566  cvgdvgrat  44289  binomcxplemnotnn0  44332  founiiun0  45171  supxrge  45321  suplesup  45322  supxrunb3  45382  lptre2pt  45625  0ellimcdiv  45634  limclner  45636  limsuppnfdlem  45686  limsuppnflem  45695  limsupmnflem  45705  liminfreuzlem  45787  liminflimsupclim  45792  cnrefiisplem  45814  climxlim2lem  45830  xlimliminflimsup  45847  icccncfext  45872  cncfiooiccre  45880  fperdvper  45904  dvnprodlem2  45932  iblcncfioo  45963  stoweidlem35  46020  wallispilem3  46052  fourierdlem20  46112  fourierdlem34  46126  fourierdlem39  46131  fourierdlem42  46134  fourierdlem46  46137  fourierdlem48  46139  fourierdlem49  46140  fourierdlem63  46154  fourierdlem64  46155  fourierdlem73  46164  fourierdlem87  46178  fourierdlem97  46188  fourierdlem103  46194  fourierdlem104  46195  fourierdlem111  46202  etransclem32  46251  etransclem33  46252  etransclem35  46254  sge0cl  46366  sge0f1o  46367  sge0split  46394  sge0iunmptlemre  46400  sge0rpcpnf  46406  sge0xadd  46420  nnfoctbdjlem  46440  ismeannd  46452  omeiunltfirp  46504  hoidmvlelem3  46582  hoidmvle  46585  ovncvr2  46596  hspdifhsp  46601  hspmbllem2  46612  ovnsubadd2lem  46630  pimdecfgtioo  46702  pimincfltioo  46703  smflimlem1  46756  smflimmpt  46795  smfpimne2  46825  resccat  49063  aacllem  49790