Theorem adantllr 718

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 679	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  750  ad4ant134  1171  ad5ant145  1366  oewordri  8201  marypha1lem  8881  rlimsqzlem  14997  fsumrlim  15158  fsumo1  15159  lcmdvds  15942  dfgrp3lem  18189  tgcl  21574  neindisj  21722  neiptoptop  21736  isr0  22342  cnextcn  22672  ustuqtop4  22850  mbfsup  24268  itg2i1fseqle  24358  ditgsplit  24464  itgulm  25003  leibpi  25528  dchrisumlem3  26075  legov  26379  legov2  26380  legtrid  26385  colopp  26563  f1otrg  26665  cusgrsize2inds  27243  grpoidinvlem3  28289  grpoideu  28292  grporcan  28301  blocni  28588  normcan  29359  unoplin  29703  hmoplin  29725  nmophmi  29814  mdslmd3i  30115  chirredlem1  30173  chirredlem2  30174  mdsymlem5  30190  cdj1i  30216  opreu2reuALT  30247  fpwrelmap  30495  fsumiunle  30571  ccatf1  30651  wrdt2ind  30653  archiabllem1  30872  archiabl  30877  isarchiofld  30941  ringlsmss1  31003  ringlsmss2  31004  rhmimaidl  31017  isprmidlc  31031  fedgmul  31115  locfinreflem  31193  pstmxmet  31250  ordtconnlem1  31277  esumcvg  31455  esum2d  31462  esumiun  31463  ldgenpisyslem1  31532  omssubadd  31668  signstfvneq0  31952  circlemeth  32021  elicc3  33778  knoppcnlem9  33953  pibt2  34834  lindsenlbs  35052  matunitlindflem1  35053  poimirlem17  35074  poimirlem20  35077  poimirlem27  35084  poimirlem29  35086  poimir  35090  heicant  35092  itg2addnclem  35108  ftc1anclem5  35134  ftc1anclem6  35135  ftc1anclem7  35136  ftc1anclem8  35137  ftc1anc  35138  fzmul  35179  fdc  35183  fdc1  35184  incsequz2  35187  rrncmslem  35270  ghomco  35329  rngoisocnv  35419  ispridlc  35508  fsuppind  39456  cvgdvgrat  41017  binomcxplemnotnn0  41060  founiiun0  41817  supxrge  41970  suplesup  41971  supxrunb3  42036  lptre2pt  42282  0ellimcdiv  42291  limclner  42293  limsuppnfdlem  42343  limsuppnflem  42352  limsupmnflem  42362  liminfreuzlem  42444  liminflimsupclim  42449  cnrefiisplem  42471  climxlim2lem  42487  xlimliminflimsup  42504  icccncfext  42529  cncfiooiccre  42537  fperdvper  42561  dvnprodlem2  42589  iblcncfioo  42620  stoweidlem35  42677  wallispilem3  42709  fourierdlem20  42769  fourierdlem34  42783  fourierdlem39  42788  fourierdlem42  42791  fourierdlem46  42794  fourierdlem48  42796  fourierdlem49  42797  fourierdlem63  42811  fourierdlem64  42812  fourierdlem73  42821  fourierdlem87  42835  fourierdlem97  42845  fourierdlem103  42851  fourierdlem104  42852  fourierdlem111  42859  etransclem32  42908  etransclem33  42909  etransclem35  42911  sge0cl  43020  sge0f1o  43021  sge0split  43048  sge0iunmptlemre  43054  sge0rpcpnf  43060  sge0xadd  43074  nnfoctbdjlem  43094  ismeannd  43106  omeiunltfirp  43158  hoidmvlelem3  43236  hoidmvle  43239  ovncvr2  43250  hspdifhsp  43255  hspmbllem2  43266  ovnsubadd2lem  43284  pimdecfgtioo  43352  pimincfltioo  43353  smflimlem1  43404  smflimmpt  43441  aacllem  45329