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  8559  marypha1lem  9391  rlimsqzlem  15622  fsumrlim  15784  fsumo1  15785  lcmdvds  16585  dfgrp3lem  18977  tgcl  22863  neindisj  23011  neiptoptop  23025  isr0  23631  cnextcn  23961  ustuqtop4  24139  mpomulcn  24765  mbfsup  25572  itg2i1fseqle  25662  ditgsplit  25769  itgulm  26324  leibpi  26859  dchrisumlem3  27409  legov  28519  legov2  28520  legtrid  28525  colopp  28703  f1otrg  28805  cusgrsize2inds  29388  grpoidinvlem3  30442  grpoideu  30445  grporcan  30454  blocni  30741  normcan  31512  unoplin  31856  hmoplin  31878  nmophmi  31967  mdslmd3i  32268  chirredlem1  32326  chirredlem2  32327  mdsymlem5  32343  cdj1i  32369  opreu2reuALT  32413  fpwrelmap  32663  fsumiunle  32761  ccatf1  32877  wrdt2ind  32882  chnind  32944  gsumwrd2dccatlem  33013  archiabllem1  33154  archiabl  33159  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnlem4  33203  elrgspnsubrunlem2  33206  isarchiofld  33302  ringlsmss1  33374  ringlsmss2  33375  nsgqusf1olem1  33391  nsgqusf1olem2  33392  nsgqusf1olem3  33393  rhmimaidl  33410  isprmidlc  33425  fedgmul  33634  irngnzply1  33693  locfinreflem  33837  pstmxmet  33894  ordtconnlem1  33921  esumcvg  34083  esum2d  34090  esumiun  34091  ldgenpisyslem1  34160  omssubadd  34298  signstfvneq0  34570  circlemeth  34638  elicc3  36312  knoppcnlem9  36496  pibt2  37412  lindsenlbs  37616  matunitlindflem1  37617  poimirlem17  37638  poimirlem20  37641  poimirlem27  37648  poimirlem29  37650  poimir  37654  heicant  37656  itg2addnclem  37672  ftc1anclem5  37698  ftc1anclem6  37699  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  fzmul  37742  fdc  37746  fdc1  37747  incsequz2  37750  rrncmslem  37833  ghomco  37892  rngoisocnv  37982  ispridlc  38071  fiabv  42531  selvvvval  42580  fsuppind  42585  cvgdvgrat  44309  binomcxplemnotnn0  44352  founiiun0  45191  supxrge  45341  suplesup  45342  supxrunb3  45402  lptre2pt  45645  0ellimcdiv  45654  limclner  45656  limsuppnfdlem  45706  limsuppnflem  45715  limsupmnflem  45725  liminfreuzlem  45807  liminflimsupclim  45812  cnrefiisplem  45834  climxlim2lem  45850  xlimliminflimsup  45867  icccncfext  45892  cncfiooiccre  45900  fperdvper  45924  dvnprodlem2  45952  iblcncfioo  45983  stoweidlem35  46040  wallispilem3  46072  fourierdlem20  46132  fourierdlem34  46146  fourierdlem39  46151  fourierdlem42  46154  fourierdlem46  46157  fourierdlem48  46159  fourierdlem49  46160  fourierdlem63  46174  fourierdlem64  46175  fourierdlem73  46184  fourierdlem87  46198  fourierdlem97  46208  fourierdlem103  46214  fourierdlem104  46215  fourierdlem111  46222  etransclem32  46271  etransclem33  46272  etransclem35  46274  sge0cl  46386  sge0f1o  46387  sge0split  46414  sge0iunmptlemre  46420  sge0rpcpnf  46426  sge0xadd  46440  nnfoctbdjlem  46460  ismeannd  46472  omeiunltfirp  46524  hoidmvlelem3  46602  hoidmvle  46605  ovncvr2  46616  hspdifhsp  46621  hspmbllem2  46632  ovnsubadd2lem  46650  pimdecfgtioo  46722  pimincfltioo  46723  smflimlem1  46776  smflimmpt  46815  smfpimne2  46845  resccat  49067  aacllem  49794