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  7153  peano5  7833  f1o2ndf1  8062  cantnfle  9578  cantnflem1c  9594  ttukeylem5  10421  rlimsqzlem  15570  dvdslcmf  16556  poslubmo  18330  posglbmo  18331  smndex1mgm  18830  isgrpinv  18921  ghmgrp  18994  dprdfcntz  19944  pzriprnglem4  21437  sraassab  21821  cply1coe0bi  22244  evls1fpws  22311  isnrm3  23301  cnextcn  24009  ustexsym  24158  ustex2sym  24159  ustex3sym  24160  trust  24171  fmucnd  24233  trcfilu  24235  metust  24500  cxpmul2z  26654  umgrres1lem  29332  upgrres1  29335  friendshipgt3  30422  ccatf1  32980  cyc3evpm  33181  elrgspnlem1  33273  elrgspnlem2  33274  elrgspnlem4  33276  elrgspnsubrunlem1  33278  elrgspnsubrunlem2  33279  znfermltl  33396  rhmimaidl  33462  evlextv  33656  dimlssid  33738  txomap  33940  zart0  33985  repr0  34717  breprexplemc  34738  hgt750lemb  34762  satffunlem1lem2  35546  satffunlem2lem2  35549  lindsadd  37753  matunitlindflem1  37756  nadd1suc  43576  mapss2  45391  supxrge  45525  xrlexaddrp  45539  infxr  45553  infleinf  45558  unb2ltle  45601  supminfxr  45650  limsuppnfdlem  45887  limsupub  45890  limsuppnflem  45896  climinf3  45902  limsupmnflem  45906  climxrre  45936  liminfvalxr  45969  fperdvper  46105  sge0isum  46613  sge0gtfsumgt  46629  sge0seq  46632  nnfoctbdjlem  46641  meaiuninc3v  46670  omeiunltfirp  46705  hspdifhsp  46802  hspmbllem2  46813  pimdecfgtioo  46903  pimincfltioo  46904  preimageiingt  46906  preimaleiinlt  46907  smfid  46938  proththd  47802