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  7183  peano5  7869  f1o2ndf1  8101  cantnfle  9624  cantnflem1c  9640  ttukeylem5  10466  rlimsqzlem  15615  dvdslcmf  16601  poslubmo  18370  posglbmo  18371  smndex1mgm  18834  isgrpinv  18925  ghmgrp  18998  dprdfcntz  19947  pzriprnglem4  21394  sraassab  21777  cply1coe0bi  22189  evls1fpws  22256  isnrm3  23246  cnextcn  23954  ustexsym  24103  ustex2sym  24104  ustex3sym  24105  trust  24117  fmucnd  24179  trcfilu  24181  metust  24446  cxpmul2z  26600  umgrres1lem  29237  upgrres1  29240  friendshipgt3  30327  ccatf1  32870  cyc3evpm  33107  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnlem4  33196  elrgspnsubrunlem1  33198  elrgspnsubrunlem2  33199  znfermltl  33337  rhmimaidl  33403  dimlssid  33628  txomap  33824  zart0  33869  repr0  34602  breprexplemc  34623  hgt750lemb  34647  satffunlem1lem2  35390  satffunlem2lem2  35393  lindsadd  37607  matunitlindflem1  37610  nadd1suc  43381  mapss2  45199  supxrge  45334  xrlexaddrp  45348  infxr  45363  infleinf  45368  unb2ltle  45411  supminfxr  45460  limsuppnfdlem  45699  limsupub  45702  limsuppnflem  45708  climinf3  45714  limsupmnflem  45718  climxrre  45748  liminfvalxr  45781  fperdvper  45917  sge0isum  46425  sge0gtfsumgt  46441  sge0seq  46444  nnfoctbdjlem  46453  meaiuninc3v  46482  omeiunltfirp  46517  hspdifhsp  46614  hspmbllem2  46625  pimdecfgtioo  46715  pimincfltioo  46716  preimageiingt  46718  preimaleiinlt  46719  smfid  46750  proththd  47615