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  1173  ad5ant145  1368  oewordri  8628  marypha1lem  9470  rlimsqzlem  15681  fsumrlim  15843  fsumo1  15844  lcmdvds  16641  dfgrp3lem  19068  tgcl  22991  neindisj  23140  neiptoptop  23154  isr0  23760  cnextcn  24090  ustuqtop4  24268  mpomulcn  24904  mbfsup  25712  itg2i1fseqle  25803  ditgsplit  25910  itgulm  26465  leibpi  26999  dchrisumlem3  27549  legov  28607  legov2  28608  legtrid  28613  colopp  28791  f1otrg  28893  cusgrsize2inds  29485  grpoidinvlem3  30534  grpoideu  30537  grporcan  30546  blocni  30833  normcan  31604  unoplin  31948  hmoplin  31970  nmophmi  32059  mdslmd3i  32360  chirredlem1  32418  chirredlem2  32419  mdsymlem5  32435  cdj1i  32461  opreu2reuALT  32504  fpwrelmap  32750  fsumiunle  32835  ccatf1  32917  wrdt2ind  32922  chnind  32984  gsumwrd2dccatlem  33051  archiabllem1  33182  archiabl  33187  elrgspnlem1  33231  elrgspnlem2  33232  elrgspnlem4  33234  isarchiofld  33326  ringlsmss1  33403  ringlsmss2  33404  nsgqusf1olem1  33420  nsgqusf1olem2  33421  nsgqusf1olem3  33422  rhmimaidl  33439  isprmidlc  33454  fedgmul  33658  irngnzply1  33705  locfinreflem  33800  pstmxmet  33857  ordtconnlem1  33884  esumcvg  34066  esum2d  34073  esumiun  34074  ldgenpisyslem1  34143  omssubadd  34281  signstfvneq0  34565  circlemeth  34633  elicc3  36299  knoppcnlem9  36483  pibt2  37399  lindsenlbs  37601  matunitlindflem1  37602  poimirlem17  37623  poimirlem20  37626  poimirlem27  37633  poimirlem29  37635  poimir  37639  heicant  37641  itg2addnclem  37657  ftc1anclem5  37683  ftc1anclem6  37684  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  fzmul  37727  fdc  37731  fdc1  37732  incsequz2  37735  rrncmslem  37818  ghomco  37877  rngoisocnv  37967  ispridlc  38056  fiabv  42522  selvvvval  42571  fsuppind  42576  cvgdvgrat  44308  binomcxplemnotnn0  44351  founiiun0  45132  supxrge  45287  suplesup  45288  supxrunb3  45348  lptre2pt  45595  0ellimcdiv  45604  limclner  45606  limsuppnfdlem  45656  limsuppnflem  45665  limsupmnflem  45675  liminfreuzlem  45757  liminflimsupclim  45762  cnrefiisplem  45784  climxlim2lem  45800  xlimliminflimsup  45817  icccncfext  45842  cncfiooiccre  45850  fperdvper  45874  dvnprodlem2  45902  iblcncfioo  45933  stoweidlem35  45990  wallispilem3  46022  fourierdlem20  46082  fourierdlem34  46096  fourierdlem39  46101  fourierdlem42  46104  fourierdlem46  46107  fourierdlem48  46109  fourierdlem49  46110  fourierdlem63  46124  fourierdlem64  46125  fourierdlem73  46134  fourierdlem87  46148  fourierdlem97  46158  fourierdlem103  46164  fourierdlem104  46165  fourierdlem111  46172  etransclem32  46221  etransclem33  46222  etransclem35  46224  sge0cl  46336  sge0f1o  46337  sge0split  46364  sge0iunmptlemre  46370  sge0rpcpnf  46376  sge0xadd  46390  nnfoctbdjlem  46410  ismeannd  46422  omeiunltfirp  46474  hoidmvlelem3  46552  hoidmvle  46555  ovncvr2  46566  hspdifhsp  46571  hspmbllem2  46582  ovnsubadd2lem  46600  pimdecfgtioo  46672  pimincfltioo  46673  smflimlem1  46726  smflimmpt  46765  smfpimne2  46795  aacllem  49031