Theorem adantllr 725

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 686	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 208  df-an 397

This theorem is referenced by:  ad4ant13  757  ad4ant134  1181  ad5ant145  1377  oewordri  8525  marypha1lem  9343  rlimsqzlem  15609  fsumrlim  15772  fsumo1  15773  lcmdvds  16575  chnind  18585  dfgrp3lem  19012  selvvvval  22125  tgcl  22959  neindisj  23107  neiptoptop  23121  isr0  23727  cnextcn  24057  ustuqtop4  24234  mpomulcn  24859  mbfsup  25656  itg2i1fseqle  25746  ditgsplit  25853  itgulm  26398  leibpi  26931  dchrisumlem3  27479  legov  28678  legov2  28679  legtrid  28684  colopp  28862  f1otrg  28964  cusgrsize2inds  29547  grpoidinvlem3  30602  grpoideu  30605  grporcan  30614  blocni  30901  normcan  31672  unoplin  32016  hmoplin  32038  nmophmi  32127  mdslmd3i  32428  chirredlem1  32486  chirredlem2  32487  mdsymlem5  32503  cdj1i  32529  opreu2reuALT  32571  fpwrelmap  32832  fsumiunle  32928  ccatf1  33035  wrdt2ind  33039  suppgsumssiun  33160  gsumwrd2dccatlem  33165  archiabllem1  33281  archiabl  33286  isarchiofld  33287  elrgspnlem1  33330  elrgspnlem2  33331  elrgspnlem4  33333  elrgspnsubrunlem2  33336  ringlsmss1  33486  ringlsmss2  33487  nsgqusf1olem1  33503  nsgqusf1olem2  33504  nsgqusf1olem3  33505  rhmimaidl  33522  isprmidlc  33537  mplvrpmrhm  33738  esplyfv1  33760  esplyfval1  33764  fedgmul  33822  irngnzply1  33882  locfinreflem  34031  pstmxmet  34088  ordtconnlem1  34115  esumcvg  34277  esum2d  34284  esumiun  34285  ldgenpisyslem1  34354  omssubadd  34491  signstfvneq0  34763  circlemeth  34831  elicc3  36552  knoppcnlem9  36814  pibt2  37786  lindsenlbs  37989  matunitlindflem1  37990  poimirlem17  38011  poimirlem20  38014  poimirlem27  38021  poimirlem29  38023  poimir  38027  heicant  38029  itg2addnclem  38045  ftc1anclem5  38071  ftc1anclem6  38072  ftc1anclem7  38073  ftc1anclem8  38074  ftc1anc  38075  fzmul  38115  fdc  38119  fdc1  38120  incsequz2  38123  rrncmslem  38206  ghomco  38265  rngoisocnv  38355  ispridlc  38444  fiabv  43029  fsuppind  43047  cvgdvgrat  44764  binomcxplemnotnn0  44807  founiiun0  45644  supxrge  45790  suplesup  45791  supxrunb3  45850  lptre2pt  46090  0ellimcdiv  46099  limclner  46101  limsuppnfdlem  46151  limsuppnflem  46160  limsupmnflem  46170  liminfreuzlem  46252  liminflimsupclim  46257  cnrefiisplem  46279  climxlim2lem  46295  xlimliminflimsup  46312  icccncfext  46337  cncfiooiccre  46345  fperdvper  46369  dvnprodlem2  46397  iblcncfioo  46428  stoweidlem35  46485  wallispilem3  46517  fourierdlem20  46577  fourierdlem34  46591  fourierdlem39  46596  fourierdlem42  46599  fourierdlem46  46602  fourierdlem48  46604  fourierdlem49  46605  fourierdlem63  46619  fourierdlem64  46620  fourierdlem73  46629  fourierdlem87  46643  fourierdlem97  46653  fourierdlem103  46659  fourierdlem104  46660  fourierdlem111  46667  etransclem32  46716  etransclem33  46717  etransclem35  46719  sge0cl  46831  sge0f1o  46832  sge0split  46859  sge0iunmptlemre  46865  sge0rpcpnf  46871  sge0xadd  46885  nnfoctbdjlem  46905  ismeannd  46917  omeiunltfirp  46969  hoidmvlelem3  47047  hoidmvle  47050  ovncvr2  47061  hspdifhsp  47066  hspmbllem2  47077  ovnsubadd2lem  47095  pimdecfgtioo  47167  pimincfltioo  47168  smflimlem1  47221  smflimmpt  47260  smfpimne2  47290  resccat  49571  aacllem  50298