Theorem adantllr 729

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  ad4ant13  761  ad4ant134  1187  ad5ant145  1387  oewordri  8555  marypha1lem  9372  rlimsqzlem  15666  fsumrlim  15829  fsumo1  15830  lcmdvds  16632  chnind  18643  dfgrp3lem  19070  selvvvval  22182  tgcl  23016  neindisj  23164  neiptoptop  23178  isr0  23784  cnextcn  24114  ustuqtop4  24291  mpomulcn  24916  mbfsup  25713  itg2i1fseqle  25803  ditgsplit  25910  itgulm  26458  leibpi  26994  dchrisumlem3  27542  legov  28741  legov2  28742  legtrid  28747  colopp  28925  f1otrg  29027  cusgrsize2inds  29610  grpoidinvlem3  30665  grpoideu  30668  grporcan  30677  blocni  30964  normcan  31735  unoplin  32079  hmoplin  32101  nmophmi  32190  mdslmd3i  32491  chirredlem1  32549  chirredlem2  32550  mdsymlem5  32566  cdj1i  32592  opreu2reuALT  32634  fpwrelmap  32895  fsumiunle  32991  ccatf1  33087  wrdt2ind  33091  suppgsumssiun  33212  gsumwrd2dccatlem  33217  archiabllem1  33333  archiabl  33338  isarchiofld  33339  elrgspnlem1  33383  elrgspnlem2  33384  elrgspnlem4  33386  elrgspnsubrunlem2  33389  ringlsmss1  33542  ringlsmss2  33543  nsgqusf1olem1  33559  nsgqusf1olem2  33560  nsgqusf1olem3  33561  rhmimaidl  33578  isprmidlc  33593  mplvrpmrhm  33804  esplyfv1  33826  esplyfval1  33830  fedgmul  33888  irngnzply1  33948  locfinreflem  34097  pstmxmet  34154  ordtconnlem1  34181  esumcvg  34343  esum2d  34350  esumiun  34351  ldgenpisyslem1  34420  omssubadd  34557  signstfvneq0  34826  circlemeth  34894  elicc3  36637  knoppcnlem9  36899  pibt2  37871  lindsenlbs  38074  matunitlindflem1  38075  poimirlem17  38096  poimirlem20  38099  poimirlem27  38106  poimirlem29  38108  poimir  38112  heicant  38114  itg2addnclem  38130  ftc1anclem5  38156  ftc1anclem6  38157  ftc1anclem7  38158  ftc1anclem8  38159  ftc1anc  38160  fzmul  38200  fdc  38204  fdc1  38205  incsequz2  38208  rrncmslem  38291  ghomco  38350  rngoisocnv  38440  ispridlc  38529  fiabv  43114  fsuppind  43132  cvgdvgrat  44849  binomcxplemnotnn0  44892  founiiun0  45728  supxrge  45874  suplesup  45875  supxrunb3  45934  lptre2pt  46174  0ellimcdiv  46183  limclner  46185  limsuppnfdlem  46235  limsuppnflem  46244  limsupmnflem  46254  liminfreuzlem  46336  liminflimsupclim  46341  cnrefiisplem  46363  climxlim2lem  46379  xlimliminflimsup  46396  icccncfext  46421  cncfiooiccre  46429  fperdvper  46453  dvnprodlem2  46481  iblcncfioo  46512  stoweidlem35  46569  wallispilem3  46601  fourierdlem20  46661  fourierdlem34  46675  fourierdlem39  46680  fourierdlem42  46683  fourierdlem46  46686  fourierdlem48  46688  fourierdlem49  46689  fourierdlem63  46703  fourierdlem64  46704  fourierdlem73  46713  fourierdlem87  46727  fourierdlem97  46737  fourierdlem103  46743  fourierdlem104  46744  fourierdlem111  46751  etransclem32  46800  etransclem33  46801  etransclem35  46803  sge0cl  46915  sge0f1o  46916  sge0split  46943  sge0iunmptlemre  46949  sge0rpcpnf  46955  sge0xadd  46969  nnfoctbdjlem  46989  ismeannd  47001  omeiunltfirp  47053  hoidmvlelem3  47131  hoidmvle  47134  ovncvr2  47145  hspdifhsp  47150  hspmbllem2  47161  ovnsubadd2lem  47179  pimdecfgtioo  47251  pimincfltioo  47252  smflimlem1  47305  smflimmpt  47344  smfpimne2  47374  resccat  49655  aacllem  50382