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  8521  marypha1lem  9339  rlimsqzlem  15602  fsumrlim  15765  fsumo1  15766  lcmdvds  16568  chnind  18578  dfgrp3lem  19005  tgcl  22944  neindisj  23092  neiptoptop  23106  isr0  23712  cnextcn  24042  ustuqtop4  24219  mpomulcn  24844  mbfsup  25641  itg2i1fseqle  25731  ditgsplit  25838  itgulm  26386  leibpi  26919  dchrisumlem3  27468  legov  28667  legov2  28668  legtrid  28673  colopp  28851  f1otrg  28953  cusgrsize2inds  29537  grpoidinvlem3  30592  grpoideu  30595  grporcan  30604  blocni  30891  normcan  31662  unoplin  32006  hmoplin  32028  nmophmi  32117  mdslmd3i  32418  chirredlem1  32476  chirredlem2  32477  mdsymlem5  32493  cdj1i  32519  opreu2reuALT  32561  fpwrelmap  32821  fsumiunle  32917  ccatf1  33024  wrdt2ind  33028  suppgsumssiun  33148  gsumwrd2dccatlem  33153  archiabllem1  33269  archiabl  33274  isarchiofld  33275  elrgspnlem1  33318  elrgspnlem2  33319  elrgspnlem4  33321  elrgspnsubrunlem2  33324  ringlsmss1  33471  ringlsmss2  33472  nsgqusf1olem1  33488  nsgqusf1olem2  33489  nsgqusf1olem3  33490  rhmimaidl  33507  isprmidlc  33522  mplvrpmrhm  33706  esplyfv1  33728  esplyfval1  33732  fedgmul  33791  irngnzply1  33851  locfinreflem  34000  pstmxmet  34057  ordtconnlem1  34084  esumcvg  34246  esum2d  34253  esumiun  34254  ldgenpisyslem1  34323  omssubadd  34460  signstfvneq0  34732  circlemeth  34800  elicc3  36515  knoppcnlem9  36777  pibt2  37747  lindsenlbs  37950  matunitlindflem1  37951  poimirlem17  37972  poimirlem20  37975  poimirlem27  37982  poimirlem29  37984  poimir  37988  heicant  37990  itg2addnclem  38006  ftc1anclem5  38032  ftc1anclem6  38033  ftc1anclem7  38034  ftc1anclem8  38035  ftc1anc  38036  fzmul  38076  fdc  38080  fdc1  38081  incsequz2  38084  rrncmslem  38167  ghomco  38226  rngoisocnv  38316  ispridlc  38405  fiabv  42995  selvvvval  43032  fsuppind  43037  cvgdvgrat  44758  binomcxplemnotnn0  44801  founiiun0  45638  supxrge  45786  suplesup  45787  supxrunb3  45846  lptre2pt  46086  0ellimcdiv  46095  limclner  46097  limsuppnfdlem  46147  limsuppnflem  46156  limsupmnflem  46166  liminfreuzlem  46248  liminflimsupclim  46253  cnrefiisplem  46275  climxlim2lem  46291  xlimliminflimsup  46308  icccncfext  46333  cncfiooiccre  46341  fperdvper  46365  dvnprodlem2  46393  iblcncfioo  46424  stoweidlem35  46481  wallispilem3  46513  fourierdlem20  46573  fourierdlem34  46587  fourierdlem39  46592  fourierdlem42  46595  fourierdlem46  46598  fourierdlem48  46600  fourierdlem49  46601  fourierdlem63  46615  fourierdlem64  46616  fourierdlem73  46625  fourierdlem87  46639  fourierdlem97  46649  fourierdlem103  46655  fourierdlem104  46656  fourierdlem111  46663  etransclem32  46712  etransclem33  46713  etransclem35  46715  sge0cl  46827  sge0f1o  46828  sge0split  46855  sge0iunmptlemre  46861  sge0rpcpnf  46867  sge0xadd  46881  nnfoctbdjlem  46901  ismeannd  46913  omeiunltfirp  46965  hoidmvlelem3  47043  hoidmvle  47046  ovncvr2  47057  hspdifhsp  47062  hspmbllem2  47073  ovnsubadd2lem  47091  pimdecfgtioo  47163  pimincfltioo  47164  smflimlem1  47217  smflimmpt  47256  smfpimne2  47286  resccat  49561  aacllem  50288