Theorem ad4ant13 764

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad5ant14  770  ad5ant24  773  ad5ant124  1388  fntpb  7214  peano5  7896  f1o2ndf1  8123  cantnfle  9647  cantnflem1c  9663  ttukeylem5  10512  ccatf1  14646  rlimsqzlem  15724  dvdslcmf  16711  poslubmo  18487  posglbmo  18488  smndex1mgm  19006  isgrpinv  19104  ghmgrp  19176  dprdfcntz  20131  pzriprnglem4  21684  sraassab  22068  cply1coe0bi  22512  evls1fpws  22579  isnrm3  23566  cnextcn  24275  ustexsym  24424  ustex2sym  24425  ustex3sym  24426  trust  24437  fmucnd  24499  trcfilu  24501  metust  24766  cxpmul2z  26907  umgrres1lem  29718  upgrres1  29721  friendshipgt3  30820  cyc3evpm  33534  elrgspnlem1  33626  elrgspnlem2  33627  elrgspnlem4  33629  elrgspnsubrunlem1  33631  elrgspnsubrunlem2  33632  znfermltl  33745  rhmimaidl  33804  selvply1rhmlema  33972  evlextv  33996  dimlssid  34086  txomap  34288  zart0  34333  repr0  35063  breprexplemc  35084  hgt750lemb  35108  satffunlem1lem2  35932  satffunlem2lem2  35935  lindsadd  38321  matunitlindflem1  38324  nadd1suc  44177  mapss2  45980  supxrge  46112  xrlexaddrp  46126  infxr  46140  infleinf  46145  unb2ltle  46187  supminfxr  46236  limsuppnfdlem  46473  limsupub  46476  limsuppnflem  46482  climinf3  46488  limsupmnflem  46492  climxrre  46522  liminfvalxr  46555  fperdvper  46691  sge0isum  47199  sge0gtfsumgt  47215  sge0seq  47218  nnfoctbdjlem  47227  meaiuninc3v  47256  omeiunltfirp  47291  hspdifhsp  47388  hspmbllem2  47399  pimdecfgtioo  47489  pimincfltioo  47490  preimageiingt  47492  preimaleiinlt  47493  smfid  47524  proththd  48424