Theorem adantllr 732

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad4ant13  764  ad4ant134  1193  ad5ant145  1396  oewordri  8587  marypha1lem  9403  ccatf1  14648  rlimsqzlem  15726  fsumrlim  15889  fsumo1  15890  lcmdvds  16691  chnind  18702  dfgrp3lem  19135  isprmidlc  21509  selvvvval  22330  tgcl  23163  neindisj  23311  neiptoptop  23325  isr0  23931  cnextcn  24261  ustuqtop4  24438  mpomulcn  25063  mbfsup  25860  itg2i1fseqle  25950  ditgsplit  26057  itgulm  26608  leibpi  27144  dchrisumlem3  27692  legov  28891  legov2  28892  legtrid  28897  colopp  29088  perpprlng  29237  f1otrg  29257  cusgrsize2inds  29840  grpoidinvlem3  30895  grpoideu  30898  grporcan  30907  blocni  31194  normcan  31965  unoplin  32309  hmoplin  32331  nmophmi  32420  mdslmd3i  32721  chirredlem1  32779  chirredlem2  32780  mdsymlem5  32796  cdj1i  32822  opreu2reuALT  32860  fpwrelmap  33115  fsumiunle  33210  wrdt2ind  33306  suppgsumssiun  33423  gsumwrd2dccatlem  33428  archiabllem1  33544  archiabl  33549  isarchiofld  33550  elrgspnlem1  33593  elrgspnlem2  33594  elrgspnlem4  33596  elrgspnsubrunlem2  33599  ringlsmss1  33738  ringlsmss2  33739  nsgqusf1olem1  33753  nsgqusf1olem2  33754  nsgqusf1olem3  33755  rhmimaidl  33771  mplvrpmrhm  33968  esplyfv1  33990  esplyfval1  33994  fedgmul  34052  irngnzply1  34112  locfinreflem  34261  pstmxmet  34318  ordtconnlem1  34345  esumcvg  34507  esum2d  34514  esumiun  34515  ldgenpisyslem1  34585  omssubadd  34722  signstfvneq0  34991  circlemeth  35059  elicc3  36869  knoppcnlem9  37131  pibt2  38104  lindsenlbs  38307  matunitlindflem1  38308  poimirlem17  38329  poimirlem20  38332  poimirlem27  38339  poimirlem29  38341  poimir  38345  heicant  38347  itg2addnclem  38363  ftc1anclem5  38389  ftc1anclem6  38390  ftc1anclem7  38391  ftc1anclem8  38392  ftc1anc  38393  fzmul  38433  fdc  38437  fdc1  38438  incsequz2  38441  rrncmslem  38524  ghomco  38583  rngoisocnv  38673  ispridlc  38762  fiabv  43345  fsuppind  43363  cvgdvgrat  45064  binomcxplemnotnn0  45107  founiiun0  45949  supxrge  46095  suplesup  46096  supxrunb3  46155  lptre2pt  46395  0ellimcdiv  46404  limclner  46406  limsuppnfdlem  46456  limsuppnflem  46465  limsupmnflem  46475  liminfreuzlem  46557  liminflimsupclim  46562  cnrefiisplem  46584  climxlim2lem  46600  xlimliminflimsup  46617  icccncfext  46642  cncfiooiccre  46650  fperdvper  46674  dvnprodlem2  46702  iblcncfioo  46733  stoweidlem35  46790  wallispilem3  46822  fourierdlem20  46882  fourierdlem34  46896  fourierdlem39  46901  fourierdlem42  46904  fourierdlem46  46907  fourierdlem48  46909  fourierdlem49  46910  fourierdlem63  46924  fourierdlem64  46925  fourierdlem73  46934  fourierdlem87  46948  fourierdlem97  46958  fourierdlem103  46964  fourierdlem104  46965  fourierdlem111  46972  etransclem32  47021  etransclem33  47022  etransclem35  47024  sge0cl  47136  sge0f1o  47137  sge0split  47164  sge0iunmptlemre  47170  sge0rpcpnf  47176  sge0xadd  47190  nnfoctbdjlem  47210  ismeannd  47222  omeiunltfirp  47274  hoidmvlelem3  47352  hoidmvle  47355  ovncvr2  47366  hspdifhsp  47371  hspmbllem2  47382  ovnsubadd2lem  47400  pimdecfgtioo  47472  pimincfltioo  47473  smflimlem1  47526  smflimmpt  47565  smfpimne2  47595  resccat  49893  aacllem  50662