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  8520  marypha1lem  9336  rlimsqzlem  15572  fsumrlim  15734  fsumo1  15735  lcmdvds  16535  chnind  18544  dfgrp3lem  18968  tgcl  22913  neindisj  23061  neiptoptop  23075  isr0  23681  cnextcn  24011  ustuqtop4  24188  mpomulcn  24814  mbfsup  25621  itg2i1fseqle  25711  ditgsplit  25818  itgulm  26373  leibpi  26908  dchrisumlem3  27458  legov  28657  legov2  28658  legtrid  28663  colopp  28841  f1otrg  28943  cusgrsize2inds  29527  grpoidinvlem3  30581  grpoideu  30584  grporcan  30593  blocni  30880  normcan  31651  unoplin  31995  hmoplin  32017  nmophmi  32106  mdslmd3i  32407  chirredlem1  32465  chirredlem2  32466  mdsymlem5  32482  cdj1i  32508  opreu2reuALT  32551  fpwrelmap  32812  fsumiunle  32910  ccatf1  33031  wrdt2ind  33035  gsumwrd2dccatlem  33159  archiabllem1  33275  archiabl  33280  isarchiofld  33281  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem4  33327  elrgspnsubrunlem2  33330  ringlsmss1  33477  ringlsmss2  33478  nsgqusf1olem1  33494  nsgqusf1olem2  33495  nsgqusf1olem3  33496  rhmimaidl  33513  isprmidlc  33528  mplvrpmrhm  33712  esplyfv1  33727  fedgmul  33788  irngnzply1  33848  locfinreflem  33997  pstmxmet  34054  ordtconnlem1  34081  esumcvg  34243  esum2d  34250  esumiun  34251  ldgenpisyslem1  34320  omssubadd  34457  signstfvneq0  34729  circlemeth  34797  elicc3  36511  knoppcnlem9  36701  pibt2  37618  lindsenlbs  37812  matunitlindflem1  37813  poimirlem17  37834  poimirlem20  37837  poimirlem27  37844  poimirlem29  37846  poimir  37850  heicant  37852  itg2addnclem  37868  ftc1anclem5  37894  ftc1anclem6  37895  ftc1anclem7  37896  ftc1anclem8  37897  ftc1anc  37898  fzmul  37938  fdc  37942  fdc1  37943  incsequz2  37946  rrncmslem  38029  ghomco  38088  rngoisocnv  38178  ispridlc  38267  fiabv  42787  selvvvval  42824  fsuppind  42829  cvgdvgrat  44550  binomcxplemnotnn0  44593  founiiun0  45430  supxrge  45579  suplesup  45580  supxrunb3  45639  lptre2pt  45880  0ellimcdiv  45889  limclner  45891  limsuppnfdlem  45941  limsuppnflem  45950  limsupmnflem  45960  liminfreuzlem  46042  liminflimsupclim  46047  cnrefiisplem  46069  climxlim2lem  46085  xlimliminflimsup  46102  icccncfext  46127  cncfiooiccre  46135  fperdvper  46159  dvnprodlem2  46187  iblcncfioo  46218  stoweidlem35  46275  wallispilem3  46307  fourierdlem20  46367  fourierdlem34  46381  fourierdlem39  46386  fourierdlem42  46389  fourierdlem46  46392  fourierdlem48  46394  fourierdlem49  46395  fourierdlem63  46409  fourierdlem64  46410  fourierdlem73  46419  fourierdlem87  46433  fourierdlem97  46443  fourierdlem103  46449  fourierdlem104  46450  fourierdlem111  46457  etransclem32  46506  etransclem33  46507  etransclem35  46509  sge0cl  46621  sge0f1o  46622  sge0split  46649  sge0iunmptlemre  46655  sge0rpcpnf  46661  sge0xadd  46675  nnfoctbdjlem  46695  ismeannd  46707  omeiunltfirp  46759  hoidmvlelem3  46837  hoidmvle  46840  ovncvr2  46851  hspdifhsp  46856  hspmbllem2  46867  ovnsubadd2lem  46885  pimdecfgtioo  46957  pimincfltioo  46958  smflimlem1  47011  smflimmpt  47050  smfpimne2  47080  resccat  49315  aacllem  50042