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  758  ad5ant24  761  fntpb  7229  peano5  7916  f1o2ndf1  8146  cantnfle  9709  cantnflem1c  9725  ttukeylem5  10551  rlimsqzlem  15682  dvdslcmf  16665  poslubmo  18469  posglbmo  18470  smndex1mgm  18933  isgrpinv  19024  ghmgrp  19097  dprdfcntz  20050  pzriprnglem4  21513  sraassab  21906  cply1coe0bi  22322  evls1fpws  22389  isnrm3  23383  cnextcn  24091  ustexsym  24240  ustex2sym  24241  ustex3sym  24242  trust  24254  fmucnd  24317  trcfilu  24319  metust  24587  cxpmul2z  26748  umgrres1lem  29342  upgrres1  29345  friendshipgt3  30427  ccatf1  32918  cyc3evpm  33153  elrgspnlem1  33232  elrgspnlem2  33233  elrgspnlem4  33235  znfermltl  33374  rhmimaidl  33440  dimlssid  33660  txomap  33795  zart0  33840  repr0  34605  breprexplemc  34626  hgt750lemb  34650  satffunlem1lem2  35388  satffunlem2lem2  35391  lindsadd  37600  matunitlindflem1  37603  nadd1suc  43382  mapss2  45148  supxrge  45288  xrlexaddrp  45302  infxr  45317  infleinf  45322  unb2ltle  45365  supminfxr  45414  limsuppnfdlem  45657  limsupub  45660  limsuppnflem  45666  climinf3  45672  limsupmnflem  45676  climxrre  45706  liminfvalxr  45739  fperdvper  45875  sge0isum  46383  sge0gtfsumgt  46399  sge0seq  46402  nnfoctbdjlem  46411  meaiuninc3v  46440  omeiunltfirp  46475  hspdifhsp  46572  hspmbllem2  46583  pimdecfgtioo  46673  pimincfltioo  46674  preimageiingt  46676  preimaleiinlt  46677  smfid  46708  proththd  47539