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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  ad4ant13  749  ad4ant134  1174  ad5ant145  1369  oewordri  8544  marypha1lem  9378  rlimsqzlem  15545  fsumrlim  15707  fsumo1  15708  lcmdvds  16495  dfgrp3lem  18859  tgcl  22356  neindisj  22505  neiptoptop  22519  isr0  23125  cnextcn  23455  ustuqtop4  23633  mbfsup  25065  itg2i1fseqle  25156  ditgsplit  25262  itgulm  25804  leibpi  26329  dchrisumlem3  26876  legov  27590  legov2  27591  legtrid  27596  colopp  27774  f1otrg  27876  cusgrsize2inds  28464  grpoidinvlem3  29511  grpoideu  29514  grporcan  29523  blocni  29810  normcan  30581  unoplin  30925  hmoplin  30947  nmophmi  31036  mdslmd3i  31337  chirredlem1  31395  chirredlem2  31396  mdsymlem5  31412  cdj1i  31438  opreu2reuALT  31469  fpwrelmap  31718  fsumiunle  31795  ccatf1  31875  wrdt2ind  31877  archiabllem1  32099  archiabl  32104  isarchiofld  32183  ringlsmss1  32250  ringlsmss2  32251  nsgqusf1olem1  32265  nsgqusf1olem2  32266  nsgqusf1olem3  32267  rhmimaidl  32282  isprmidlc  32296  fedgmul  32413  irngnzply1  32452  locfinreflem  32510  pstmxmet  32567  ordtconnlem1  32594  esumcvg  32774  esum2d  32781  esumiun  32782  ldgenpisyslem1  32851  omssubadd  32989  signstfvneq0  33273  circlemeth  33342  elicc3  34865  knoppcnlem9  35040  pibt2  35961  lindsenlbs  36146  matunitlindflem1  36147  poimirlem17  36168  poimirlem20  36171  poimirlem27  36178  poimirlem29  36180  poimir  36184  heicant  36186  itg2addnclem  36202  ftc1anclem5  36228  ftc1anclem6  36229  ftc1anclem7  36230  ftc1anclem8  36231  ftc1anc  36232  fzmul  36273  fdc  36277  fdc1  36278  incsequz2  36281  rrncmslem  36364  ghomco  36423  rngoisocnv  36513  ispridlc  36602  fsuppind  40823  cvgdvgrat  42715  binomcxplemnotnn0  42758  founiiun0  43531  supxrge  43693  suplesup  43694  supxrunb3  43754  lptre2pt  44001  0ellimcdiv  44010  limclner  44012  limsuppnfdlem  44062  limsuppnflem  44071  limsupmnflem  44081  liminfreuzlem  44163  liminflimsupclim  44168  cnrefiisplem  44190  climxlim2lem  44206  xlimliminflimsup  44223  icccncfext  44248  cncfiooiccre  44256  fperdvper  44280  dvnprodlem2  44308  iblcncfioo  44339  stoweidlem35  44396  wallispilem3  44428  fourierdlem20  44488  fourierdlem34  44502  fourierdlem39  44507  fourierdlem42  44510  fourierdlem46  44513  fourierdlem48  44515  fourierdlem49  44516  fourierdlem63  44530  fourierdlem64  44531  fourierdlem73  44540  fourierdlem87  44554  fourierdlem97  44564  fourierdlem103  44570  fourierdlem104  44571  fourierdlem111  44578  etransclem32  44627  etransclem33  44628  etransclem35  44630  sge0cl  44742  sge0f1o  44743  sge0split  44770  sge0iunmptlemre  44776  sge0rpcpnf  44782  sge0xadd  44796  nnfoctbdjlem  44816  ismeannd  44828  omeiunltfirp  44880  hoidmvlelem3  44958  hoidmvle  44961  ovncvr2  44972  hspdifhsp  44977  hspmbllem2  44988  ovnsubadd2lem  45006  pimdecfgtioo  45078  pimincfltioo  45079  smflimlem1  45132  smflimmpt  45171  smfpimne2  45201  aacllem  47368