Theorem adantllr 715

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 676	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 206  df-an 396

This theorem is referenced by:  ad4ant13  747  ad4ant134  1172  ad5ant145  1367  oewordri  8385  marypha1lem  9122  rlimsqzlem  15288  fsumrlim  15451  fsumo1  15452  lcmdvds  16241  dfgrp3lem  18588  tgcl  22027  neindisj  22176  neiptoptop  22190  isr0  22796  cnextcn  23126  ustuqtop4  23304  mbfsup  24733  itg2i1fseqle  24824  ditgsplit  24930  itgulm  25472  leibpi  25997  dchrisumlem3  26544  legov  26850  legov2  26851  legtrid  26856  colopp  27034  f1otrg  27136  cusgrsize2inds  27723  grpoidinvlem3  28769  grpoideu  28772  grporcan  28781  blocni  29068  normcan  29839  unoplin  30183  hmoplin  30205  nmophmi  30294  mdslmd3i  30595  chirredlem1  30653  chirredlem2  30654  mdsymlem5  30670  cdj1i  30696  opreu2reuALT  30726  fpwrelmap  30970  fsumiunle  31045  ccatf1  31125  wrdt2ind  31127  archiabllem1  31349  archiabl  31354  isarchiofld  31418  ringlsmss1  31486  ringlsmss2  31487  nsgqusf1olem1  31500  nsgqusf1olem2  31501  nsgqusf1olem3  31502  rhmimaidl  31511  isprmidlc  31525  fedgmul  31614  locfinreflem  31692  pstmxmet  31749  ordtconnlem1  31776  esumcvg  31954  esum2d  31961  esumiun  31962  ldgenpisyslem1  32031  omssubadd  32167  signstfvneq0  32451  circlemeth  32520  elicc3  34433  knoppcnlem9  34608  pibt2  35515  lindsenlbs  35699  matunitlindflem1  35700  poimirlem17  35721  poimirlem20  35724  poimirlem27  35731  poimirlem29  35733  poimir  35737  heicant  35739  itg2addnclem  35755  ftc1anclem5  35781  ftc1anclem6  35782  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  fzmul  35826  fdc  35830  fdc1  35831  incsequz2  35834  rrncmslem  35917  ghomco  35976  rngoisocnv  36066  ispridlc  36155  fsuppind  40202  cvgdvgrat  41820  binomcxplemnotnn0  41863  founiiun0  42617  supxrge  42767  suplesup  42768  supxrunb3  42829  lptre2pt  43071  0ellimcdiv  43080  limclner  43082  limsuppnfdlem  43132  limsuppnflem  43141  limsupmnflem  43151  liminfreuzlem  43233  liminflimsupclim  43238  cnrefiisplem  43260  climxlim2lem  43276  xlimliminflimsup  43293  icccncfext  43318  cncfiooiccre  43326  fperdvper  43350  dvnprodlem2  43378  iblcncfioo  43409  stoweidlem35  43466  wallispilem3  43498  fourierdlem20  43558  fourierdlem34  43572  fourierdlem39  43577  fourierdlem42  43580  fourierdlem46  43583  fourierdlem48  43585  fourierdlem49  43586  fourierdlem63  43600  fourierdlem64  43601  fourierdlem73  43610  fourierdlem87  43624  fourierdlem97  43634  fourierdlem103  43640  fourierdlem104  43641  fourierdlem111  43648  etransclem32  43697  etransclem33  43698  etransclem35  43700  sge0cl  43809  sge0f1o  43810  sge0split  43837  sge0iunmptlemre  43843  sge0rpcpnf  43849  sge0xadd  43863  nnfoctbdjlem  43883  ismeannd  43895  omeiunltfirp  43947  hoidmvlelem3  44025  hoidmvle  44028  ovncvr2  44039  hspdifhsp  44044  hspmbllem2  44055  ovnsubadd2lem  44073  pimdecfgtioo  44141  pimincfltioo  44142  smflimlem1  44193  smflimmpt  44230  aacllem  46391