Theorem adantllr 731

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ad4ant13  763  ad4ant134  1193  ad5ant145  1396  oewordri  8579  marypha1lem  9394  rlimsqzlem  15702  fsumrlim  15865  fsumo1  15866  lcmdvds  16667  chnind  18678  dfgrp3lem  19105  isprmidlc  21453  selvvvval  22274  tgcl  23107  neindisj  23255  neiptoptop  23269  isr0  23875  cnextcn  24205  ustuqtop4  24382  mpomulcn  25007  mbfsup  25804  itg2i1fseqle  25894  ditgsplit  26001  itgulm  26552  leibpi  27088  dchrisumlem3  27636  legov  28835  legov2  28836  legtrid  28841  colopp  29032  perpprlng  29181  f1otrg  29201  cusgrsize2inds  29784  grpoidinvlem3  30839  grpoideu  30842  grporcan  30851  blocni  31138  normcan  31909  unoplin  32253  hmoplin  32275  nmophmi  32364  mdslmd3i  32665  chirredlem1  32723  chirredlem2  32724  mdsymlem5  32740  cdj1i  32766  opreu2reuALT  32804  fpwrelmap  33059  fsumiunle  33154  ccatf1  33250  wrdt2ind  33254  suppgsumssiun  33373  gsumwrd2dccatlem  33378  archiabllem1  33494  archiabl  33499  isarchiofld  33500  elrgspnlem1  33543  elrgspnlem2  33544  elrgspnlem4  33546  elrgspnsubrunlem2  33549  ringlsmss1  33688  ringlsmss2  33689  nsgqusf1olem1  33703  nsgqusf1olem2  33704  nsgqusf1olem3  33705  rhmimaidl  33721  mplvrpmrhm  33918  esplyfv1  33940  esplyfval1  33944  fedgmul  34002  irngnzply1  34062  locfinreflem  34211  pstmxmet  34268  ordtconnlem1  34295  esumcvg  34457  esum2d  34464  esumiun  34465  ldgenpisyslem1  34534  omssubadd  34671  signstfvneq0  34940  circlemeth  35008  elicc3  36809  knoppcnlem9  37071  pibt2  38044  lindsenlbs  38247  matunitlindflem1  38248  poimirlem17  38269  poimirlem20  38272  poimirlem27  38279  poimirlem29  38281  poimir  38285  heicant  38287  itg2addnclem  38303  ftc1anclem5  38329  ftc1anclem6  38330  ftc1anclem7  38331  ftc1anclem8  38332  ftc1anc  38333  fzmul  38373  fdc  38377  fdc1  38378  incsequz2  38381  rrncmslem  38464  ghomco  38523  rngoisocnv  38613  ispridlc  38702  fiabv  43287  fsuppind  43305  cvgdvgrat  45006  binomcxplemnotnn0  45049  founiiun0  45891  supxrge  46037  suplesup  46038  supxrunb3  46097  lptre2pt  46337  0ellimcdiv  46346  limclner  46348  limsuppnfdlem  46398  limsuppnflem  46407  limsupmnflem  46417  liminfreuzlem  46499  liminflimsupclim  46504  cnrefiisplem  46526  climxlim2lem  46542  xlimliminflimsup  46559  icccncfext  46584  cncfiooiccre  46592  fperdvper  46616  dvnprodlem2  46644  iblcncfioo  46675  stoweidlem35  46732  wallispilem3  46764  fourierdlem20  46824  fourierdlem34  46838  fourierdlem39  46843  fourierdlem42  46846  fourierdlem46  46849  fourierdlem48  46851  fourierdlem49  46852  fourierdlem63  46866  fourierdlem64  46867  fourierdlem73  46876  fourierdlem87  46890  fourierdlem97  46900  fourierdlem103  46906  fourierdlem104  46907  fourierdlem111  46914  etransclem32  46963  etransclem33  46964  etransclem35  46966  sge0cl  47078  sge0f1o  47079  sge0split  47106  sge0iunmptlemre  47112  sge0rpcpnf  47118  sge0xadd  47132  nnfoctbdjlem  47152  ismeannd  47164  omeiunltfirp  47216  hoidmvlelem3  47294  hoidmvle  47297  ovncvr2  47308  hspdifhsp  47313  hspmbllem2  47324  ovnsubadd2lem  47342  pimdecfgtioo  47414  pimincfltioo  47415  smflimlem1  47468  smflimmpt  47507  smfpimne2  47537  resccat  49835  aacllem  50584