Theorem adantllr 720

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 681	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  752  ad4ant134  1176  ad5ant145  1372  oewordri  8530  marypha1lem  9348  rlimsqzlem  15584  fsumrlim  15746  fsumo1  15747  lcmdvds  16547  chnind  18556  dfgrp3lem  18980  tgcl  22925  neindisj  23073  neiptoptop  23087  isr0  23693  cnextcn  24023  ustuqtop4  24200  mpomulcn  24826  mbfsup  25633  itg2i1fseqle  25723  ditgsplit  25830  itgulm  26385  leibpi  26920  dchrisumlem3  27470  legov  28669  legov2  28670  legtrid  28675  colopp  28853  f1otrg  28955  cusgrsize2inds  29539  grpoidinvlem3  30593  grpoideu  30596  grporcan  30605  blocni  30892  normcan  31663  unoplin  32007  hmoplin  32029  nmophmi  32118  mdslmd3i  32419  chirredlem1  32477  chirredlem2  32478  mdsymlem5  32494  cdj1i  32520  opreu2reuALT  32562  fpwrelmap  32822  fsumiunle  32920  ccatf1  33041  wrdt2ind  33045  suppgsumssiun  33165  gsumwrd2dccatlem  33170  archiabllem1  33286  archiabl  33291  isarchiofld  33292  elrgspnlem1  33335  elrgspnlem2  33336  elrgspnlem4  33338  elrgspnsubrunlem2  33341  ringlsmss1  33488  ringlsmss2  33489  nsgqusf1olem1  33505  nsgqusf1olem2  33506  nsgqusf1olem3  33507  rhmimaidl  33524  isprmidlc  33539  mplvrpmrhm  33723  esplyfv1  33745  esplyfval1  33749  fedgmul  33808  irngnzply1  33868  locfinreflem  34017  pstmxmet  34074  ordtconnlem1  34101  esumcvg  34263  esum2d  34270  esumiun  34271  ldgenpisyslem1  34340  omssubadd  34477  signstfvneq0  34749  circlemeth  34817  elicc3  36530  knoppcnlem9  36720  pibt2  37669  lindsenlbs  37863  matunitlindflem1  37864  poimirlem17  37885  poimirlem20  37888  poimirlem27  37895  poimirlem29  37897  poimir  37901  heicant  37903  itg2addnclem  37919  ftc1anclem5  37945  ftc1anclem6  37946  ftc1anclem7  37947  ftc1anclem8  37948  ftc1anc  37949  fzmul  37989  fdc  37993  fdc1  37994  incsequz2  37997  rrncmslem  38080  ghomco  38139  rngoisocnv  38229  ispridlc  38318  fiabv  42903  selvvvval  42940  fsuppind  42945  cvgdvgrat  44666  binomcxplemnotnn0  44709  founiiun0  45546  supxrge  45694  suplesup  45695  supxrunb3  45754  lptre2pt  45995  0ellimcdiv  46004  limclner  46006  limsuppnfdlem  46056  limsuppnflem  46065  limsupmnflem  46075  liminfreuzlem  46157  liminflimsupclim  46162  cnrefiisplem  46184  climxlim2lem  46200  xlimliminflimsup  46217  icccncfext  46242  cncfiooiccre  46250  fperdvper  46274  dvnprodlem2  46302  iblcncfioo  46333  stoweidlem35  46390  wallispilem3  46422  fourierdlem20  46482  fourierdlem34  46496  fourierdlem39  46501  fourierdlem42  46504  fourierdlem46  46507  fourierdlem48  46509  fourierdlem49  46510  fourierdlem63  46524  fourierdlem64  46525  fourierdlem73  46534  fourierdlem87  46548  fourierdlem97  46558  fourierdlem103  46564  fourierdlem104  46565  fourierdlem111  46572  etransclem32  46621  etransclem33  46622  etransclem35  46624  sge0cl  46736  sge0f1o  46737  sge0split  46764  sge0iunmptlemre  46770  sge0rpcpnf  46776  sge0xadd  46790  nnfoctbdjlem  46810  ismeannd  46822  omeiunltfirp  46874  hoidmvlelem3  46952  hoidmvle  46955  ovncvr2  46966  hspdifhsp  46971  hspmbllem2  46982  ovnsubadd2lem  47000  pimdecfgtioo  47072  pimincfltioo  47073  smflimlem1  47126  smflimmpt  47165  smfpimne2  47195  resccat  49430  aacllem  50157