Theorem adantllr 717

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  ad4ant13  749  ad4ant134  1170  ad5ant145  1365  r19.29anOLD  3332  oewordri  8212  marypha1lem  8891  rlimsqzlem  14999  fsumrlim  15160  fsumo1  15161  lcmdvds  15946  dfgrp3lem  18191  tgcl  21571  neindisj  21719  neiptoptop  21733  isr0  22339  cnextcn  22669  ustuqtop4  22847  mbfsup  24259  itg2i1fseqle  24349  ditgsplit  24453  itgulm  24990  leibpi  25514  dchrisumlem3  26061  legov  26365  legov2  26366  legtrid  26371  colopp  26549  f1otrg  26651  cusgrsize2inds  27229  grpoidinvlem3  28277  grpoideu  28280  grporcan  28289  blocni  28576  normcan  29347  unoplin  29691  hmoplin  29713  nmophmi  29802  mdslmd3i  30103  chirredlem1  30161  chirredlem2  30162  mdsymlem5  30178  cdj1i  30204  opreu2reuALT  30234  fpwrelmap  30463  fsumiunle  30540  ccatf1  30620  wrdt2ind  30622  archiabllem1  30817  archiabl  30822  isarchiofld  30885  isprmidlc  30958  fedgmul  31022  locfinreflem  31099  pstmxmet  31132  ordtconnlem1  31162  esumcvg  31340  esum2d  31347  esumiun  31348  ldgenpisyslem1  31417  omssubadd  31553  signstfvneq0  31837  circlemeth  31906  elicc3  33660  knoppcnlem9  33835  pibt2  34692  lindsenlbs  34881  matunitlindflem1  34882  poimirlem17  34903  poimirlem20  34906  poimirlem27  34913  poimirlem29  34915  poimir  34919  heicant  34921  itg2addnclem  34937  ftc1anclem5  34965  ftc1anclem6  34966  ftc1anclem7  34967  ftc1anclem8  34968  ftc1anc  34969  fzmul  35010  fdc  35014  fdc1  35015  incsequz2  35018  rrncmslem  35104  ghomco  35163  rngoisocnv  35253  ispridlc  35342  cvgdvgrat  40638  binomcxplemnotnn0  40681  founiiun0  41444  supxrge  41599  suplesup  41600  supxrunb3  41665  lptre2pt  41914  0ellimcdiv  41923  limclner  41925  limsuppnfdlem  41975  limsuppnflem  41984  limsupmnflem  41994  liminfreuzlem  42076  liminflimsupclim  42081  cnrefiisplem  42103  climxlim2lem  42119  xlimliminflimsup  42136  icccncfext  42163  cncfiooiccre  42171  fperdvper  42196  dvnprodlem2  42225  iblcncfioo  42256  stoweidlem35  42314  wallispilem3  42346  fourierdlem20  42406  fourierdlem34  42420  fourierdlem39  42425  fourierdlem42  42428  fourierdlem46  42431  fourierdlem48  42433  fourierdlem49  42434  fourierdlem63  42448  fourierdlem64  42449  fourierdlem73  42458  fourierdlem87  42472  fourierdlem97  42482  fourierdlem103  42488  fourierdlem104  42489  fourierdlem111  42496  etransclem32  42545  etransclem33  42546  etransclem35  42548  sge0cl  42657  sge0f1o  42658  sge0split  42685  sge0iunmptlemre  42691  sge0rpcpnf  42697  sge0xadd  42711  nnfoctbdjlem  42731  ismeannd  42743  omeiunltfirp  42795  hoidmvlelem3  42873  hoidmvle  42876  ovncvr2  42887  hspdifhsp  42892  hspmbllem2  42903  ovnsubadd2lem  42921  pimdecfgtioo  42989  pimincfltioo  42990  smflimlem1  43041  smflimmpt  43078  aacllem  44896