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  7155  peano5  7835  f1o2ndf1  8064  cantnfle  9580  cantnflem1c  9596  ttukeylem5  10423  rlimsqzlem  15572  dvdslcmf  16558  poslubmo  18332  posglbmo  18333  smndex1mgm  18832  isgrpinv  18923  ghmgrp  18996  dprdfcntz  19946  pzriprnglem4  21439  sraassab  21823  cply1coe0bi  22246  evls1fpws  22313  isnrm3  23303  cnextcn  24011  ustexsym  24160  ustex2sym  24161  ustex3sym  24162  trust  24173  fmucnd  24235  trcfilu  24237  metust  24502  cxpmul2z  26656  umgrres1lem  29383  upgrres1  29386  friendshipgt3  30473  ccatf1  33031  cyc3evpm  33232  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem4  33327  elrgspnsubrunlem1  33329  elrgspnsubrunlem2  33330  znfermltl  33447  rhmimaidl  33513  evlextv  33707  dimlssid  33789  txomap  33991  zart0  34036  repr0  34768  breprexplemc  34789  hgt750lemb  34813  satffunlem1lem2  35597  satffunlem2lem2  35600  lindsadd  37814  matunitlindflem1  37817  nadd1suc  43634  mapss2  45449  supxrge  45583  xrlexaddrp  45597  infxr  45611  infleinf  45616  unb2ltle  45659  supminfxr  45708  limsuppnfdlem  45945  limsupub  45948  limsuppnflem  45954  climinf3  45960  limsupmnflem  45964  climxrre  45994  liminfvalxr  46027  fperdvper  46163  sge0isum  46671  sge0gtfsumgt  46687  sge0seq  46690  nnfoctbdjlem  46699  meaiuninc3v  46728  omeiunltfirp  46763  hspdifhsp  46860  hspmbllem2  46871  pimdecfgtioo  46961  pimincfltioo  46962  preimageiingt  46964  preimaleiinlt  46965  smfid  46996  proththd  47860