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  8630  marypha1lem  9473  rlimsqzlem  15685  fsumrlim  15847  fsumo1  15848  lcmdvds  16645  dfgrp3lem  19056  tgcl  22976  neindisj  23125  neiptoptop  23139  isr0  23745  cnextcn  24075  ustuqtop4  24253  mpomulcn  24891  mbfsup  25699  itg2i1fseqle  25789  ditgsplit  25896  itgulm  26451  leibpi  26985  dchrisumlem3  27535  legov  28593  legov2  28594  legtrid  28599  colopp  28777  f1otrg  28879  cusgrsize2inds  29471  grpoidinvlem3  30525  grpoideu  30528  grporcan  30537  blocni  30824  normcan  31595  unoplin  31939  hmoplin  31961  nmophmi  32050  mdslmd3i  32351  chirredlem1  32409  chirredlem2  32410  mdsymlem5  32426  cdj1i  32452  opreu2reuALT  32496  fpwrelmap  32744  fsumiunle  32831  ccatf1  32933  wrdt2ind  32938  chnind  33001  gsumwrd2dccatlem  33069  archiabllem1  33200  archiabl  33205  elrgspnlem1  33246  elrgspnlem2  33247  elrgspnlem4  33249  elrgspnsubrunlem2  33252  isarchiofld  33347  ringlsmss1  33424  ringlsmss2  33425  nsgqusf1olem1  33441  nsgqusf1olem2  33442  nsgqusf1olem3  33443  rhmimaidl  33460  isprmidlc  33475  fedgmul  33682  irngnzply1  33741  locfinreflem  33839  pstmxmet  33896  ordtconnlem1  33923  esumcvg  34087  esum2d  34094  esumiun  34095  ldgenpisyslem1  34164  omssubadd  34302  signstfvneq0  34587  circlemeth  34655  elicc3  36318  knoppcnlem9  36502  pibt2  37418  lindsenlbs  37622  matunitlindflem1  37623  poimirlem17  37644  poimirlem20  37647  poimirlem27  37654  poimirlem29  37656  poimir  37660  heicant  37662  itg2addnclem  37678  ftc1anclem5  37704  ftc1anclem6  37705  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  fzmul  37748  fdc  37752  fdc1  37753  incsequz2  37756  rrncmslem  37839  ghomco  37898  rngoisocnv  37988  ispridlc  38077  fiabv  42546  selvvvval  42595  fsuppind  42600  cvgdvgrat  44332  binomcxplemnotnn0  44375  founiiun0  45195  supxrge  45349  suplesup  45350  supxrunb3  45410  lptre2pt  45655  0ellimcdiv  45664  limclner  45666  limsuppnfdlem  45716  limsuppnflem  45725  limsupmnflem  45735  liminfreuzlem  45817  liminflimsupclim  45822  cnrefiisplem  45844  climxlim2lem  45860  xlimliminflimsup  45877  icccncfext  45902  cncfiooiccre  45910  fperdvper  45934  dvnprodlem2  45962  iblcncfioo  45993  stoweidlem35  46050  wallispilem3  46082  fourierdlem20  46142  fourierdlem34  46156  fourierdlem39  46161  fourierdlem42  46164  fourierdlem46  46167  fourierdlem48  46169  fourierdlem49  46170  fourierdlem63  46184  fourierdlem64  46185  fourierdlem73  46194  fourierdlem87  46208  fourierdlem97  46218  fourierdlem103  46224  fourierdlem104  46225  fourierdlem111  46232  etransclem32  46281  etransclem33  46282  etransclem35  46284  sge0cl  46396  sge0f1o  46397  sge0split  46424  sge0iunmptlemre  46430  sge0rpcpnf  46436  sge0xadd  46450  nnfoctbdjlem  46470  ismeannd  46482  omeiunltfirp  46534  hoidmvlelem3  46612  hoidmvle  46615  ovncvr2  46626  hspdifhsp  46631  hspmbllem2  46642  ovnsubadd2lem  46660  pimdecfgtioo  46732  pimincfltioo  46733  smflimlem1  46786  smflimmpt  46825  smfpimne2  46855  aacllem  49320