Theorem ad4ant13 757

Description: Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)

Hypothesis

Ref	Expression
ad4ant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
ad4ant13	⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜓) ∧ 𝜏) → 𝜒)

Proof of Theorem ad4ant13

Step	Hyp	Ref	Expression
1		ad4ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantr 481	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜒)
3	2	adantllr 725	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:  ad5ant14  763  ad5ant24  766  fntpb  7153  peano5  7833  f1o2ndf1  8061  cantnfle  9583  cantnflem1c  9599  ttukeylem5  10426  rlimsqzlem  15602  dvdslcmf  16591  poslubmo  18366  posglbmo  18367  smndex1mgm  18869  isgrpinv  18960  ghmgrp  19033  dprdfcntz  19983  pzriprnglem4  21459  sraassab  21843  cply1coe0bi  22288  evls1fpws  22355  isnrm3  23342  cnextcn  24050  ustexsym  24199  ustex2sym  24200  ustex3sym  24201  trust  24212  fmucnd  24274  trcfilu  24276  metust  24541  cxpmul2z  26673  umgrres1lem  29397  upgrres1  29400  friendshipgt3  30486  ccatf1  33028  cyc3evpm  33231  elrgspnlem1  33323  elrgspnlem2  33324  elrgspnlem4  33326  elrgspnsubrunlem1  33328  elrgspnsubrunlem2  33329  znfermltl  33449  rhmimaidl  33515  selvply1rhmlema  33702  evlextv  33726  dimlssid  33816  txomap  34018  zart0  34063  repr0  34795  breprexplemc  34816  hgt750lemb  34840  satffunlem1lem2  35631  satffunlem2lem2  35634  lindsadd  37980  matunitlindflem1  37983  nadd1suc  43837  mapss2  45651  supxrge  45783  xrlexaddrp  45797  infxr  45811  infleinf  45816  unb2ltle  45858  supminfxr  45907  limsuppnfdlem  46144  limsupub  46147  limsuppnflem  46153  climinf3  46159  limsupmnflem  46163  climxrre  46193  liminfvalxr  46226  fperdvper  46362  sge0isum  46870  sge0gtfsumgt  46886  sge0seq  46889  nnfoctbdjlem  46898  meaiuninc3v  46927  omeiunltfirp  46962  hspdifhsp  47059  hspmbllem2  47070  pimdecfgtioo  47160  pimincfltioo  47161  preimageiingt  47163  preimaleiinlt  47164  smfid  47195  proththd  48092