Theorem ad4ant13 764

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 486	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜒)
3	2	adantllr 732	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:  ad5ant14  770  ad5ant24  773  ad5ant124  1388  fntpb  7213  peano5  7903  f1o2ndf1  8131  cantnfle  9665  cantnflem1c  9681  ttukeylem5  10584  ccatf1  14729  rlimsqzlem  15809  dvdslcmf  16799  poslubmo  18576  posglbmo  18577  smndex1mgm  19099  isgrpinv  19197  ghmgrp  19269  dprdfcntz  20224  pzriprnglem4  21783  sraassab  22169  cply1coe0bi  22613  evls1fpws  22680  matunitlindflem1  22987  isnrm3  23670  cnextcn  24379  ustexsym  24528  ustex2sym  24529  ustex3sym  24530  trust  24541  fmucnd  24603  trcfilu  24605  metust  24870  cxpmul2z  27012  umgrres1lem  29884  upgrres1  29887  friendshipgt3  30992  cyc3evpm  33704  elrgspnlem1  33796  elrgspnlem2  33797  elrgspnlem4  33799  elrgspnsubrunlem1  33801  elrgspnsubrunlem2  33802  znfermltl  33915  rhmimaidl  33975  selvply1rhmlema  34143  evlextv  34167  dimlssid  34257  txomap  34459  zart0  34504  repr0  35233  breprexplemc  35254  hgt750lemb  35278  satffunlem1lem2  36147  satffunlem2lem2  36150  lindsadd  38516  nadd1suc  44378  mapss2  46188  supxrge  46319  xrlexaddrp  46333  infxr  46347  infleinf  46352  unb2ltle  46394  supminfxr  46443  limsuppnfdlem  46680  limsupub  46683  limsuppnflem  46689  climinf3  46695  limsupmnflem  46699  climxrre  46729  liminfvalxr  46762  fperdvper  46898  sge0isum  47406  sge0gtfsumgt  47422  sge0seq  47425  nnfoctbdjlem  47434  meaiuninc3v  47463  omeiunltfirp  47498  hspdifhsp  47595  hspmbllem2  47606  pimdecfgtioo  47696  pimincfltioo  47697  preimageiingt  47699  preimaleiinlt  47700  smfid  47731  proththd  48668