Theorem adantllr 731

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 487	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜑)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl1 692	1 ⊢ ((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ad4ant13  763  ad4ant134  1191  ad5ant145  1392  oewordri  8566  marypha1lem  9381  rlimsqzlem  15688  fsumrlim  15851  fsumo1  15852  lcmdvds  16654  chnind  18665  dfgrp3lem  19092  isprmidlc  21431  selvvvval  22250  tgcl  23083  neindisj  23231  neiptoptop  23245  isr0  23851  cnextcn  24181  ustuqtop4  24358  mpomulcn  24983  mbfsup  25780  itg2i1fseqle  25870  ditgsplit  25977  itgulm  26525  leibpi  27061  dchrisumlem3  27609  legov  28808  legov2  28809  legtrid  28814  colopp  28996  f1otrg  29125  cusgrsize2inds  29708  grpoidinvlem3  30763  grpoideu  30766  grporcan  30775  blocni  31062  normcan  31833  unoplin  32177  hmoplin  32199  nmophmi  32288  mdslmd3i  32589  chirredlem1  32647  chirredlem2  32648  mdsymlem5  32664  cdj1i  32690  opreu2reuALT  32729  fpwrelmap  32986  fsumiunle  33081  ccatf1  33177  wrdt2ind  33181  suppgsumssiun  33300  gsumwrd2dccatlem  33305  archiabllem1  33421  archiabl  33426  isarchiofld  33427  elrgspnlem1  33470  elrgspnlem2  33471  elrgspnlem4  33473  elrgspnsubrunlem2  33476  ringlsmss1  33618  ringlsmss2  33619  nsgqusf1olem1  33633  nsgqusf1olem2  33634  nsgqusf1olem3  33635  rhmimaidl  33651  mplvrpmrhm  33849  esplyfv1  33871  esplyfval1  33875  fedgmul  33933  irngnzply1  33993  locfinreflem  34142  pstmxmet  34199  ordtconnlem1  34226  esumcvg  34388  esum2d  34395  esumiun  34396  ldgenpisyslem1  34465  omssubadd  34602  signstfvneq0  34871  circlemeth  34939  elicc3  36685  knoppcnlem9  36947  pibt2  37918  lindsenlbs  38121  matunitlindflem1  38122  poimirlem17  38143  poimirlem20  38146  poimirlem27  38153  poimirlem29  38155  poimir  38159  heicant  38161  itg2addnclem  38177  ftc1anclem5  38203  ftc1anclem6  38204  ftc1anclem7  38205  ftc1anclem8  38206  ftc1anc  38207  fzmul  38247  fdc  38251  fdc1  38252  incsequz2  38255  rrncmslem  38338  ghomco  38397  rngoisocnv  38487  ispridlc  38576  fiabv  43161  fsuppind  43179  cvgdvgrat  44882  binomcxplemnotnn0  44925  founiiun0  45767  supxrge  45913  suplesup  45914  supxrunb3  45973  lptre2pt  46213  0ellimcdiv  46222  limclner  46224  limsuppnfdlem  46274  limsuppnflem  46283  limsupmnflem  46293  liminfreuzlem  46375  liminflimsupclim  46380  cnrefiisplem  46402  climxlim2lem  46418  xlimliminflimsup  46435  icccncfext  46460  cncfiooiccre  46468  fperdvper  46492  dvnprodlem2  46520  iblcncfioo  46551  stoweidlem35  46608  wallispilem3  46640  fourierdlem20  46700  fourierdlem34  46714  fourierdlem39  46719  fourierdlem42  46722  fourierdlem46  46725  fourierdlem48  46727  fourierdlem49  46728  fourierdlem63  46742  fourierdlem64  46743  fourierdlem73  46752  fourierdlem87  46766  fourierdlem97  46776  fourierdlem103  46782  fourierdlem104  46783  fourierdlem111  46790  etransclem32  46839  etransclem33  46840  etransclem35  46842  sge0cl  46954  sge0f1o  46955  sge0split  46982  sge0iunmptlemre  46988  sge0rpcpnf  46994  sge0xadd  47008  nnfoctbdjlem  47028  ismeannd  47040  omeiunltfirp  47092  hoidmvlelem3  47170  hoidmvle  47173  ovncvr2  47184  hspdifhsp  47189  hspmbllem2  47200  ovnsubadd2lem  47218  pimdecfgtioo  47290  pimincfltioo  47291  smflimlem1  47344  smflimmpt  47383  smfpimne2  47413  resccat  49704  aacllem  50431