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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  ad4ant13  751  ad4ant134  1175  ad5ant145  1370  oewordri  8249  marypha1lem  8970  rlimsqzlem  15098  fsumrlim  15259  fsumo1  15260  lcmdvds  16049  dfgrp3lem  18315  tgcl  21720  neindisj  21868  neiptoptop  21882  isr0  22488  cnextcn  22818  ustuqtop4  22996  mbfsup  24416  itg2i1fseqle  24507  ditgsplit  24613  itgulm  25155  leibpi  25680  dchrisumlem3  26227  legov  26531  legov2  26532  legtrid  26537  colopp  26715  f1otrg  26817  cusgrsize2inds  27395  grpoidinvlem3  28441  grpoideu  28444  grporcan  28453  blocni  28740  normcan  29511  unoplin  29855  hmoplin  29877  nmophmi  29966  mdslmd3i  30267  chirredlem1  30325  chirredlem2  30326  mdsymlem5  30342  cdj1i  30368  opreu2reuALT  30399  fpwrelmap  30643  fsumiunle  30718  ccatf1  30798  wrdt2ind  30800  archiabllem1  31024  archiabl  31029  isarchiofld  31093  ringlsmss1  31156  ringlsmss2  31157  nsgqusf1olem1  31170  nsgqusf1olem2  31171  nsgqusf1olem3  31172  rhmimaidl  31181  isprmidlc  31195  fedgmul  31284  locfinreflem  31362  pstmxmet  31419  ordtconnlem1  31446  esumcvg  31624  esum2d  31631  esumiun  31632  ldgenpisyslem1  31701  omssubadd  31837  signstfvneq0  32121  circlemeth  32190  elicc3  34144  knoppcnlem9  34319  pibt2  35211  lindsenlbs  35395  matunitlindflem1  35396  poimirlem17  35417  poimirlem20  35420  poimirlem27  35427  poimirlem29  35429  poimir  35433  heicant  35435  itg2addnclem  35451  ftc1anclem5  35477  ftc1anclem6  35478  ftc1anclem7  35479  ftc1anclem8  35480  ftc1anc  35481  fzmul  35522  fdc  35526  fdc1  35527  incsequz2  35530  rrncmslem  35613  ghomco  35672  rngoisocnv  35762  ispridlc  35851  fsuppind  39858  cvgdvgrat  41469  binomcxplemnotnn0  41512  founiiun0  42266  supxrge  42415  suplesup  42416  supxrunb3  42477  lptre2pt  42723  0ellimcdiv  42732  limclner  42734  limsuppnfdlem  42784  limsuppnflem  42793  limsupmnflem  42803  liminfreuzlem  42885  liminflimsupclim  42890  cnrefiisplem  42912  climxlim2lem  42928  xlimliminflimsup  42945  icccncfext  42970  cncfiooiccre  42978  fperdvper  43002  dvnprodlem2  43030  iblcncfioo  43061  stoweidlem35  43118  wallispilem3  43150  fourierdlem20  43210  fourierdlem34  43224  fourierdlem39  43229  fourierdlem42  43232  fourierdlem46  43235  fourierdlem48  43237  fourierdlem49  43238  fourierdlem63  43252  fourierdlem64  43253  fourierdlem73  43262  fourierdlem87  43276  fourierdlem97  43286  fourierdlem103  43292  fourierdlem104  43293  fourierdlem111  43300  etransclem32  43349  etransclem33  43350  etransclem35  43352  sge0cl  43461  sge0f1o  43462  sge0split  43489  sge0iunmptlemre  43495  sge0rpcpnf  43501  sge0xadd  43515  nnfoctbdjlem  43535  ismeannd  43547  omeiunltfirp  43599  hoidmvlelem3  43677  hoidmvle  43680  ovncvr2  43691  hspdifhsp  43696  hspmbllem2  43707  ovnsubadd2lem  43725  pimdecfgtioo  43793  pimincfltioo  43794  smflimlem1  43845  smflimmpt  43882  aacllem  45958