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  8604  marypha1lem  9445  rlimsqzlem  15665  fsumrlim  15827  fsumo1  15828  lcmdvds  16627  dfgrp3lem  19021  tgcl  22907  neindisj  23055  neiptoptop  23069  isr0  23675  cnextcn  24005  ustuqtop4  24183  mpomulcn  24809  mbfsup  25617  itg2i1fseqle  25707  ditgsplit  25814  itgulm  26369  leibpi  26904  dchrisumlem3  27454  legov  28564  legov2  28565  legtrid  28570  colopp  28748  f1otrg  28850  cusgrsize2inds  29433  grpoidinvlem3  30487  grpoideu  30490  grporcan  30499  blocni  30786  normcan  31557  unoplin  31901  hmoplin  31923  nmophmi  32012  mdslmd3i  32313  chirredlem1  32371  chirredlem2  32372  mdsymlem5  32388  cdj1i  32414  opreu2reuALT  32458  fpwrelmap  32710  fsumiunle  32808  ccatf1  32924  wrdt2ind  32929  chnind  32991  gsumwrd2dccatlem  33060  archiabllem1  33191  archiabl  33196  elrgspnlem1  33237  elrgspnlem2  33238  elrgspnlem4  33240  elrgspnsubrunlem2  33243  isarchiofld  33339  ringlsmss1  33411  ringlsmss2  33412  nsgqusf1olem1  33428  nsgqusf1olem2  33429  nsgqusf1olem3  33430  rhmimaidl  33447  isprmidlc  33462  fedgmul  33671  irngnzply1  33732  locfinreflem  33871  pstmxmet  33928  ordtconnlem1  33955  esumcvg  34117  esum2d  34124  esumiun  34125  ldgenpisyslem1  34194  omssubadd  34332  signstfvneq0  34604  circlemeth  34672  elicc3  36335  knoppcnlem9  36519  pibt2  37435  lindsenlbs  37639  matunitlindflem1  37640  poimirlem17  37661  poimirlem20  37664  poimirlem27  37671  poimirlem29  37673  poimir  37677  heicant  37679  itg2addnclem  37695  ftc1anclem5  37721  ftc1anclem6  37722  ftc1anclem7  37723  ftc1anclem8  37724  ftc1anc  37725  fzmul  37765  fdc  37769  fdc1  37770  incsequz2  37773  rrncmslem  37856  ghomco  37915  rngoisocnv  38005  ispridlc  38094  fiabv  42559  selvvvval  42608  fsuppind  42613  cvgdvgrat  44337  binomcxplemnotnn0  44380  founiiun0  45214  supxrge  45365  suplesup  45366  supxrunb3  45426  lptre2pt  45669  0ellimcdiv  45678  limclner  45680  limsuppnfdlem  45730  limsuppnflem  45739  limsupmnflem  45749  liminfreuzlem  45831  liminflimsupclim  45836  cnrefiisplem  45858  climxlim2lem  45874  xlimliminflimsup  45891  icccncfext  45916  cncfiooiccre  45924  fperdvper  45948  dvnprodlem2  45976  iblcncfioo  46007  stoweidlem35  46064  wallispilem3  46096  fourierdlem20  46156  fourierdlem34  46170  fourierdlem39  46175  fourierdlem42  46178  fourierdlem46  46181  fourierdlem48  46183  fourierdlem49  46184  fourierdlem63  46198  fourierdlem64  46199  fourierdlem73  46208  fourierdlem87  46222  fourierdlem97  46232  fourierdlem103  46238  fourierdlem104  46239  fourierdlem111  46246  etransclem32  46295  etransclem33  46296  etransclem35  46298  sge0cl  46410  sge0f1o  46411  sge0split  46438  sge0iunmptlemre  46444  sge0rpcpnf  46450  sge0xadd  46464  nnfoctbdjlem  46484  ismeannd  46496  omeiunltfirp  46548  hoidmvlelem3  46626  hoidmvle  46629  ovncvr2  46640  hspdifhsp  46645  hspmbllem2  46656  ovnsubadd2lem  46674  pimdecfgtioo  46746  pimincfltioo  46747  smflimlem1  46800  smflimmpt  46839  smfpimne2  46869  resccat  49041  aacllem  49665