Theorem ad4ant13 751

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 480	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜒)
3	2	adantllr 719	1 ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜓) ∧ 𝜏) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ad5ant14  757  ad5ant24  760  fntpb  7230  peano5  7916  f1o2ndf1  8148  cantnfle  9712  cantnflem1c  9728  ttukeylem5  10554  rlimsqzlem  15686  dvdslcmf  16669  poslubmo  18457  posglbmo  18458  smndex1mgm  18921  isgrpinv  19012  ghmgrp  19085  dprdfcntz  20036  pzriprnglem4  21496  sraassab  21889  cply1coe0bi  22307  evls1fpws  22374  isnrm3  23368  cnextcn  24076  ustexsym  24225  ustex2sym  24226  ustex3sym  24227  trust  24239  fmucnd  24302  trcfilu  24304  metust  24572  cxpmul2z  26734  umgrres1lem  29328  upgrres1  29331  friendshipgt3  30418  ccatf1  32934  cyc3evpm  33171  elrgspnlem1  33247  elrgspnlem2  33248  elrgspnlem4  33250  elrgspnsubrunlem1  33252  elrgspnsubrunlem2  33253  znfermltl  33395  rhmimaidl  33461  dimlssid  33684  txomap  33834  zart0  33879  repr0  34627  breprexplemc  34648  hgt750lemb  34672  satffunlem1lem2  35409  satffunlem2lem2  35412  lindsadd  37621  matunitlindflem1  37624  nadd1suc  43410  mapss2  45215  supxrge  45354  xrlexaddrp  45368  infxr  45383  infleinf  45388  unb2ltle  45431  supminfxr  45480  limsuppnfdlem  45721  limsupub  45724  limsuppnflem  45730  climinf3  45736  limsupmnflem  45740  climxrre  45770  liminfvalxr  45803  fperdvper  45939  sge0isum  46447  sge0gtfsumgt  46463  sge0seq  46466  nnfoctbdjlem  46475  meaiuninc3v  46504  omeiunltfirp  46539  hspdifhsp  46636  hspmbllem2  46647  pimdecfgtioo  46737  pimincfltioo  46738  preimageiingt  46740  preimaleiinlt  46741  smfid  46772  proththd  47606