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  1389  fntpb  7246  peano5  7939  f1o2ndf1  8170  cantnfle  9709  cantnflem1c  9725  ttukeylem5  10630  ccatf1  14777  rlimsqzlem  15860  dvdslcmf  16850  poslubmo  18633  posglbmo  18634  smndex1mgm  19156  isgrpinv  19254  ghmgrp  19326  dprdfcntz  20282  pzriprnglem4  21845  sraassab  22231  cply1coe0bi  22675  evls1fpws  22742  matunitlindflem1  23049  isnrm3  23732  cnextcn  24441  ustexsym  24590  ustex2sym  24591  ustex3sym  24592  trust  24603  fmucnd  24665  trcfilu  24667  metust  24932  cxpmul2z  27076  umgrres1lem  29948  upgrres1  29951  friendshipgt3  31056  cyc3evpm  33810  elrgspnlem1  33902  elrgspnlem2  33903  elrgspnlem4  33905  elrgspnsubrunlem1  33907  elrgspnsubrunlem2  33908  znfermltl  34026  rhmimaidl  34086  selvply1rhmlema  34261  evlextv  34285  dimlssid  34375  txomap  34577  reff  34582  zart0  34622  repr0  35351  breprexplemc  35372  hgt750lemb  35396  satffunlem1lem2  36376  satffunlem2lem2  36379  lindsadd  38804  nadd1suc  44655  mapss2  46492  supxrge  46623  xrlexaddrp  46637  infxr  46651  infleinf  46656  unb2ltle  46698  supminfxr  46747  limsuppnfdlem  46984  limsupub  46987  limsuppnflem  46993  climinf3  46999  limsupmnflem  47003  climxrre  47033  liminfvalxr  47066  fperdvper  47202  sge0isum  47710  sge0gtfsumgt  47726  sge0seq  47729  nnfoctbdjlem  47738  meaiuninc3v  47767  omeiunltfirp  47802  hspdifhsp  47899  hspmbllem2  47910  pimdecfgtioo  48000  pimincfltioo  48001  preimageiingt  48003  preimaleiinlt  48004  smfid  48035  proththd  48972