Theorem ad4ant13 749

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

Syntax hints:   → wi 4   ∧ wa 398

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 399

This theorem is referenced by:  ad5ant14  756  ad5ant24  759  fntpb  6972  peano5  7605  f1o2ndf1  7818  cantnfle  9134  cantnflem1c  9150  ttukeylem5  9935  rlimsqzlem  15005  dvdslcmf  15975  poslubmo  17756  posglbmo  17757  smndex1mgm  18072  isgrpinv  18156  ghmgrp  18223  dprdfcntz  19137  cply1coe0bi  20468  isnrm3  21967  cnextcn  22675  ustexsym  22824  ustex2sym  22825  ustex3sym  22826  trust  22838  fmucnd  22901  trcfilu  22903  metust  23168  cxpmul2z  25274  umgrres1lem  27092  upgrres1  27095  friendshipgt3  28177  ccatf1  30625  cyc3evpm  30792  txomap  31098  repr0  31882  breprexplemc  31903  hgt750lemb  31927  satffunlem1lem2  32650  satffunlem2lem2  32653  lindsadd  34900  matunitlindflem1  34903  mapss2  41488  supxrge  41626  xrlexaddrp  41640  infxr  41655  infleinf  41660  unb2ltle  41709  supminfxr  41760  limsuppnfdlem  42002  limsupub  42005  limsuppnflem  42011  climinf3  42017  limsupmnflem  42021  climxrre  42051  liminfvalxr  42084  fperdvper  42223  sge0isum  42729  sge0gtfsumgt  42745  sge0seq  42748  nnfoctbdjlem  42757  meaiuninc3v  42786  omeiunltfirp  42821  hspdifhsp  42918  hspmbllem2  42929  pimdecfgtioo  43015  pimincfltioo  43016  preimageiingt  43018  preimaleiinlt  43019  smfid  43049  proththd  43799