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  7145  peano5  7826  f1o2ndf1  8055  cantnfle  9567  cantnflem1c  9583  ttukeylem5  10407  rlimsqzlem  15556  dvdslcmf  16542  poslubmo  18315  posglbmo  18316  smndex1mgm  18781  isgrpinv  18872  ghmgrp  18945  dprdfcntz  19896  pzriprnglem4  21391  sraassab  21775  cply1coe0bi  22187  evls1fpws  22254  isnrm3  23244  cnextcn  23952  ustexsym  24101  ustex2sym  24102  ustex3sym  24103  trust  24115  fmucnd  24177  trcfilu  24179  metust  24444  cxpmul2z  26598  umgrres1lem  29255  upgrres1  29258  friendshipgt3  30342  ccatf1  32890  cyc3evpm  33092  elrgspnlem1  33182  elrgspnlem2  33183  elrgspnlem4  33185  elrgspnsubrunlem1  33187  elrgspnsubrunlem2  33188  znfermltl  33303  rhmimaidl  33369  dimlssid  33599  txomap  33801  zart0  33846  repr0  34579  breprexplemc  34600  hgt750lemb  34624  satffunlem1lem2  35376  satffunlem2lem2  35379  lindsadd  37593  matunitlindflem1  37596  nadd1suc  43365  mapss2  45183  supxrge  45318  xrlexaddrp  45332  infxr  45346  infleinf  45351  unb2ltle  45394  supminfxr  45443  limsuppnfdlem  45682  limsupub  45685  limsuppnflem  45691  climinf3  45697  limsupmnflem  45701  climxrre  45731  liminfvalxr  45764  fperdvper  45900  sge0isum  46408  sge0gtfsumgt  46424  sge0seq  46427  nnfoctbdjlem  46436  meaiuninc3v  46465  omeiunltfirp  46500  hspdifhsp  46597  hspmbllem2  46608  pimdecfgtioo  46698  pimincfltioo  46699  preimageiingt  46701  preimaleiinlt  46702  smfid  46733  proththd  47598