Theorem ad4ant13 752

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 720	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  7164  peano5  7844  f1o2ndf1  8072  cantnfle  9592  cantnflem1c  9608  ttukeylem5  10435  rlimsqzlem  15611  dvdslcmf  16600  poslubmo  18375  posglbmo  18376  smndex1mgm  18878  isgrpinv  18969  ghmgrp  19042  dprdfcntz  19992  pzriprnglem4  21464  sraassab  21848  cply1coe0bi  22267  evls1fpws  22334  isnrm3  23324  cnextcn  24032  ustexsym  24181  ustex2sym  24182  ustex3sym  24183  trust  24194  fmucnd  24256  trcfilu  24258  metust  24523  cxpmul2z  26655  umgrres1lem  29379  upgrres1  29382  friendshipgt3  30468  ccatf1  33009  cyc3evpm  33211  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem4  33306  elrgspnsubrunlem1  33308  elrgspnsubrunlem2  33309  znfermltl  33426  rhmimaidl  33492  evlextv  33686  dimlssid  33776  txomap  33978  zart0  34023  repr0  34755  breprexplemc  34776  hgt750lemb  34800  satffunlem1lem2  35585  satffunlem2lem2  35588  lindsadd  37934  matunitlindflem1  37937  nadd1suc  43820  mapss2  45634  supxrge  45768  xrlexaddrp  45782  infxr  45796  infleinf  45801  unb2ltle  45843  supminfxr  45892  limsuppnfdlem  46129  limsupub  46132  limsuppnflem  46138  climinf3  46144  limsupmnflem  46148  climxrre  46178  liminfvalxr  46211  fperdvper  46347  sge0isum  46855  sge0gtfsumgt  46871  sge0seq  46874  nnfoctbdjlem  46883  meaiuninc3v  46912  omeiunltfirp  46947  hspdifhsp  47044  hspmbllem2  47055  pimdecfgtioo  47145  pimincfltioo  47146  preimageiingt  47148  preimaleiinlt  47149  smfid  47180  proththd  48077