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  8585  marypha1lem  9409  ccatf1  14716  rlimsqzlem  15796  fsumrlim  15958  fsumo1  15959  lcmdvds  16763  chnind  18775  dfgrp3lem  19228  isprmidlc  21608  lindsenlbs  22137  selvvvval  22431  matunitlindflem1  22974  tgcl  23267  neindisj  23415  neiptoptop  23429  isr0  24036  cnextcn  24366  ustuqtop4  24543  mpomulcn  25168  mbfsup  25965  itg2i1fseqle  26055  ditgsplit  26161  itgulm  26717  leibpi  27252  dchrisumlem3  27800  legov  29030  legov2  29031  legtrid  29036  colopp  29229  perpprlng  29410  f1otrg  29430  cusgrsize2inds  30016  grpoidinvlem3  31090  grpoideu  31093  grporcan  31102  blocni  31389  normcan  32160  unoplin  32504  hmoplin  32526  nmophmi  32615  mdslmd3i  32916  chirredlem1  32974  chirredlem2  32975  mdsymlem5  32991  cdj1i  33017  opreu2reuALT  33055  fpwrelmap  33307  fsumiunle  33402  wrdt2ind  33498  suppgsumssiun  33615  gsumwrd2dccatlem  33620  archiabllem1  33736  archiabl  33741  isarchiofld  33742  elrgspnlem1  33785  elrgspnlem2  33786  elrgspnlem4  33788  elrgspnsubrunlem2  33791  ringlsmss1  33931  ringlsmss2  33932  nsgqusf1olem1  33946  nsgqusf1olem2  33947  nsgqusf1olem3  33948  rhmimaidl  33964  mplvrpmrhm  34161  esplyfv1  34183  esplyfval1  34187  fedgmul  34245  irngnzply1  34305  locfinreflem  34454  pstmxmet  34511  ordtconnlem1  34538  esumcvg  34700  esum2d  34707  esumiun  34708  ldgenpisyslem1  34778  omssubadd  34915  signstfvneq0  35184  circlemeth  35252  elicc3  37075  knoppcnlem9  37337  pibt2  38308  poimirlem17  38523  poimirlem20  38526  poimirlem27  38533  poimirlem29  38535  poimir  38539  heicant  38541  itg2addnclem  38557  ftc1anclem5  38583  ftc1anclem6  38584  ftc1anclem7  38585  ftc1anclem8  38586  ftc1anc  38587  fzmul  38643  fdc  38647  fdc1  38648  incsequz2  38651  rrncmslem  38734  ghomco  38793  rngoisocnv  38883  ispridlc  38972  fiabv  43562  fsuppind  43580  cvgdvgrat  45256  binomcxplemnotnn0  45299  founiiun0  46148  supxrge  46294  suplesup  46295  supxrunb3  46354  lptre2pt  46594  0ellimcdiv  46603  limclner  46605  limsuppnfdlem  46655  limsuppnflem  46664  limsupmnflem  46674  liminfreuzlem  46756  liminflimsupclim  46761  cnrefiisplem  46783  climxlim2lem  46799  xlimliminflimsup  46816  icccncfext  46841  cncfiooiccre  46849  fperdvper  46873  dvnprodlem2  46901  iblcncfioo  46932  stoweidlem35  46989  wallispilem3  47021  fourierdlem20  47081  fourierdlem34  47095  fourierdlem39  47100  fourierdlem42  47103  fourierdlem46  47106  fourierdlem48  47108  fourierdlem49  47109  fourierdlem63  47123  fourierdlem64  47124  fourierdlem73  47133  fourierdlem87  47147  fourierdlem97  47157  fourierdlem103  47163  fourierdlem104  47164  fourierdlem111  47171  etransclem32  47220  etransclem33  47221  etransclem35  47223  sge0cl  47335  sge0f1o  47336  sge0split  47363  sge0iunmptlemre  47369  sge0rpcpnf  47375  sge0xadd  47389  nnfoctbdjlem  47409  ismeannd  47421  omeiunltfirp  47473  hoidmvlelem3  47551  hoidmvle  47554  ovncvr2  47565  hspdifhsp  47570  hspmbllem2  47581  ovnsubadd2lem  47599  pimdecfgtioo  47671  pimincfltioo  47672  smflimlem1  47725  smflimmpt  47764  smfpimne2  47794  resccat  50126  aacllem  50883