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  8556  marypha1lem  9384  rlimsqzlem  15615  fsumrlim  15777  fsumo1  15778  lcmdvds  16578  dfgrp3lem  18970  tgcl  22856  neindisj  23004  neiptoptop  23018  isr0  23624  cnextcn  23954  ustuqtop4  24132  mpomulcn  24758  mbfsup  25565  itg2i1fseqle  25655  ditgsplit  25762  itgulm  26317  leibpi  26852  dchrisumlem3  27402  legov  28512  legov2  28513  legtrid  28518  colopp  28696  f1otrg  28798  cusgrsize2inds  29381  grpoidinvlem3  30435  grpoideu  30438  grporcan  30447  blocni  30734  normcan  31505  unoplin  31849  hmoplin  31871  nmophmi  31960  mdslmd3i  32261  chirredlem1  32319  chirredlem2  32320  mdsymlem5  32336  cdj1i  32362  opreu2reuALT  32406  fpwrelmap  32656  fsumiunle  32754  ccatf1  32870  wrdt2ind  32875  chnind  32937  gsumwrd2dccatlem  33006  archiabllem1  33147  archiabl  33152  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnlem4  33196  elrgspnsubrunlem2  33199  isarchiofld  33295  ringlsmss1  33367  ringlsmss2  33368  nsgqusf1olem1  33384  nsgqusf1olem2  33385  nsgqusf1olem3  33386  rhmimaidl  33403  isprmidlc  33418  fedgmul  33627  irngnzply1  33686  locfinreflem  33830  pstmxmet  33887  ordtconnlem1  33914  esumcvg  34076  esum2d  34083  esumiun  34084  ldgenpisyslem1  34153  omssubadd  34291  signstfvneq0  34563  circlemeth  34631  elicc3  36305  knoppcnlem9  36489  pibt2  37405  lindsenlbs  37609  matunitlindflem1  37610  poimirlem17  37631  poimirlem20  37634  poimirlem27  37641  poimirlem29  37643  poimir  37647  heicant  37649  itg2addnclem  37665  ftc1anclem5  37691  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  fzmul  37735  fdc  37739  fdc1  37740  incsequz2  37743  rrncmslem  37826  ghomco  37885  rngoisocnv  37975  ispridlc  38064  fiabv  42524  selvvvval  42573  fsuppind  42578  cvgdvgrat  44302  binomcxplemnotnn0  44345  founiiun0  45184  supxrge  45334  suplesup  45335  supxrunb3  45395  lptre2pt  45638  0ellimcdiv  45647  limclner  45649  limsuppnfdlem  45699  limsuppnflem  45708  limsupmnflem  45718  liminfreuzlem  45800  liminflimsupclim  45805  cnrefiisplem  45827  climxlim2lem  45843  xlimliminflimsup  45860  icccncfext  45885  cncfiooiccre  45893  fperdvper  45917  dvnprodlem2  45945  iblcncfioo  45976  stoweidlem35  46033  wallispilem3  46065  fourierdlem20  46125  fourierdlem34  46139  fourierdlem39  46144  fourierdlem42  46147  fourierdlem46  46150  fourierdlem48  46152  fourierdlem49  46153  fourierdlem63  46167  fourierdlem64  46168  fourierdlem73  46177  fourierdlem87  46191  fourierdlem97  46201  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  etransclem32  46264  etransclem33  46265  etransclem35  46267  sge0cl  46379  sge0f1o  46380  sge0split  46407  sge0iunmptlemre  46413  sge0rpcpnf  46419  sge0xadd  46433  nnfoctbdjlem  46453  ismeannd  46465  omeiunltfirp  46517  hoidmvlelem3  46595  hoidmvle  46598  ovncvr2  46609  hspdifhsp  46614  hspmbllem2  46625  ovnsubadd2lem  46643  pimdecfgtioo  46715  pimincfltioo  46716  smflimlem1  46769  smflimmpt  46808  smfpimne2  46838  resccat  49063  aacllem  49790