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  7206  peano5  7894  f1o2ndf1  8126  cantnfle  9690  cantnflem1c  9706  ttukeylem5  10532  rlimsqzlem  15670  dvdslcmf  16655  poslubmo  18426  posglbmo  18427  smndex1mgm  18890  isgrpinv  18981  ghmgrp  19054  dprdfcntz  20003  pzriprnglem4  21450  sraassab  21833  cply1coe0bi  22245  evls1fpws  22312  isnrm3  23302  cnextcn  24010  ustexsym  24159  ustex2sym  24160  ustex3sym  24161  trust  24173  fmucnd  24235  trcfilu  24237  metust  24502  cxpmul2z  26657  umgrres1lem  29294  upgrres1  29297  friendshipgt3  30384  ccatf1  32929  cyc3evpm  33166  elrgspnlem1  33242  elrgspnlem2  33243  elrgspnlem4  33245  elrgspnsubrunlem1  33247  elrgspnsubrunlem2  33248  znfermltl  33386  rhmimaidl  33452  dimlssid  33677  txomap  33870  zart0  33915  repr0  34648  breprexplemc  34669  hgt750lemb  34693  satffunlem1lem2  35430  satffunlem2lem2  35433  lindsadd  37642  matunitlindflem1  37645  nadd1suc  43391  mapss2  45209  supxrge  45345  xrlexaddrp  45359  infxr  45374  infleinf  45379  unb2ltle  45422  supminfxr  45471  limsuppnfdlem  45710  limsupub  45713  limsuppnflem  45719  climinf3  45725  limsupmnflem  45729  climxrre  45759  liminfvalxr  45792  fperdvper  45928  sge0isum  46436  sge0gtfsumgt  46452  sge0seq  46455  nnfoctbdjlem  46464  meaiuninc3v  46493  omeiunltfirp  46528  hspdifhsp  46625  hspmbllem2  46636  pimdecfgtioo  46726  pimincfltioo  46727  preimageiingt  46729  preimaleiinlt  46730  smfid  46761  proththd  47608