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  8513  marypha1lem  9324  rlimsqzlem  15558  fsumrlim  15720  fsumo1  15721  lcmdvds  16521  chnind  18529  dfgrp3lem  18953  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  29434  grpoidinvlem3  30488  grpoideu  30491  grporcan  30500  blocni  30787  normcan  31558  unoplin  31902  hmoplin  31924  nmophmi  32013  mdslmd3i  32314  chirredlem1  32372  chirredlem2  32373  mdsymlem5  32389  cdj1i  32415  opreu2reuALT  32458  fpwrelmap  32720  fsumiunle  32817  ccatf1  32937  wrdt2ind  32941  gsumwrd2dccatlem  33053  archiabllem1  33169  archiabl  33174  isarchiofld  33175  elrgspnlem1  33216  elrgspnlem2  33217  elrgspnlem4  33219  elrgspnsubrunlem2  33222  ringlsmss1  33368  ringlsmss2  33369  nsgqusf1olem1  33385  nsgqusf1olem2  33386  nsgqusf1olem3  33387  rhmimaidl  33404  isprmidlc  33419  mplvrpmrhm  33595  esplyfv1  33609  fedgmul  33665  irngnzply1  33725  locfinreflem  33874  pstmxmet  33931  ordtconnlem1  33958  esumcvg  34120  esum2d  34127  esumiun  34128  ldgenpisyslem1  34197  omssubadd  34334  signstfvneq0  34606  circlemeth  34674  elicc3  36382  knoppcnlem9  36566  pibt2  37482  lindsenlbs  37676  matunitlindflem1  37677  poimirlem17  37698  poimirlem20  37701  poimirlem27  37708  poimirlem29  37710  poimir  37714  heicant  37716  itg2addnclem  37732  ftc1anclem5  37758  ftc1anclem6  37759  ftc1anclem7  37760  ftc1anclem8  37761  ftc1anc  37762  fzmul  37802  fdc  37806  fdc1  37807  incsequz2  37810  rrncmslem  37893  ghomco  37952  rngoisocnv  38042  ispridlc  38131  fiabv  42655  selvvvval  42704  fsuppind  42709  cvgdvgrat  44431  binomcxplemnotnn0  44474  founiiun0  45312  supxrge  45462  suplesup  45463  supxrunb3  45522  lptre2pt  45763  0ellimcdiv  45772  limclner  45774  limsuppnfdlem  45824  limsuppnflem  45833  limsupmnflem  45843  liminfreuzlem  45925  liminflimsupclim  45930  cnrefiisplem  45952  climxlim2lem  45968  xlimliminflimsup  45985  icccncfext  46010  cncfiooiccre  46018  fperdvper  46042  dvnprodlem2  46070  iblcncfioo  46101  stoweidlem35  46158  wallispilem3  46190  fourierdlem20  46250  fourierdlem34  46264  fourierdlem39  46269  fourierdlem42  46272  fourierdlem46  46275  fourierdlem48  46277  fourierdlem49  46278  fourierdlem63  46292  fourierdlem64  46293  fourierdlem73  46302  fourierdlem87  46316  fourierdlem97  46326  fourierdlem103  46332  fourierdlem104  46333  fourierdlem111  46340  etransclem32  46389  etransclem33  46390  etransclem35  46392  sge0cl  46504  sge0f1o  46505  sge0split  46532  sge0iunmptlemre  46538  sge0rpcpnf  46544  sge0xadd  46558  nnfoctbdjlem  46578  ismeannd  46590  omeiunltfirp  46642  hoidmvlelem3  46720  hoidmvle  46723  ovncvr2  46734  hspdifhsp  46739  hspmbllem2  46750  ovnsubadd2lem  46768  pimdecfgtioo  46840  pimincfltioo  46841  smflimlem1  46894  smflimmpt  46933  smfpimne2  46963  resccat  49200  aacllem  49927