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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  ad5ant14  758  ad5ant24  761  fntpb  6994  peano5  7636  peano5OLD  7637  f1o2ndf1  7856  cantnfle  9219  cantnflem1c  9235  ttukeylem5  10025  rlimsqzlem  15110  dvdslcmf  16084  poslubmo  17884  posglbmo  17885  smndex1mgm  18200  isgrpinv  18286  ghmgrp  18353  dprdfcntz  19268  cply1coe0bi  21087  isnrm3  22122  cnextcn  22830  ustexsym  22979  ustex2sym  22980  ustex3sym  22981  trust  22993  fmucnd  23056  trcfilu  23058  metust  23323  cxpmul2z  25446  umgrres1lem  27264  upgrres1  27267  friendshipgt3  28347  ccatf1  30810  cyc3evpm  31006  znfermltl  31146  rhmimaidl  31193  txomap  31368  zart0  31413  repr0  32173  breprexplemc  32194  hgt750lemb  32218  satffunlem1lem2  32948  satffunlem2lem2  32951  lindsadd  35425  matunitlindflem1  35428  mapss2  42323  supxrge  42455  xrlexaddrp  42469  infxr  42484  infleinf  42489  unb2ltle  42533  supminfxr  42584  limsuppnfdlem  42824  limsupub  42827  limsuppnflem  42833  climinf3  42839  limsupmnflem  42843  climxrre  42873  liminfvalxr  42906  fperdvper  43042  sge0isum  43547  sge0gtfsumgt  43563  sge0seq  43566  nnfoctbdjlem  43575  meaiuninc3v  43604  omeiunltfirp  43639  hspdifhsp  43736  hspmbllem2  43747  pimdecfgtioo  43833  pimincfltioo  43834  preimageiingt  43836  preimaleiinlt  43837  smfid  43867  proththd  44647