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  7165  peano5  7849  f1o2ndf1  8078  cantnfle  9600  cantnflem1c  9616  ttukeylem5  10442  rlimsqzlem  15591  dvdslcmf  16577  poslubmo  18346  posglbmo  18347  smndex1mgm  18810  isgrpinv  18901  ghmgrp  18974  dprdfcntz  19923  pzriprnglem4  21370  sraassab  21753  cply1coe0bi  22165  evls1fpws  22232  isnrm3  23222  cnextcn  23930  ustexsym  24079  ustex2sym  24080  ustex3sym  24081  trust  24093  fmucnd  24155  trcfilu  24157  metust  24422  cxpmul2z  26576  umgrres1lem  29213  upgrres1  29216  friendshipgt3  30300  ccatf1  32843  cyc3evpm  33080  elrgspnlem1  33166  elrgspnlem2  33167  elrgspnlem4  33169  elrgspnsubrunlem1  33171  elrgspnsubrunlem2  33172  znfermltl  33310  rhmimaidl  33376  dimlssid  33601  txomap  33797  zart0  33842  repr0  34575  breprexplemc  34596  hgt750lemb  34620  satffunlem1lem2  35363  satffunlem2lem2  35366  lindsadd  37580  matunitlindflem1  37583  nadd1suc  43354  mapss2  45172  supxrge  45307  xrlexaddrp  45321  infxr  45336  infleinf  45341  unb2ltle  45384  supminfxr  45433  limsuppnfdlem  45672  limsupub  45675  limsuppnflem  45681  climinf3  45687  limsupmnflem  45691  climxrre  45721  liminfvalxr  45754  fperdvper  45890  sge0isum  46398  sge0gtfsumgt  46414  sge0seq  46417  nnfoctbdjlem  46426  meaiuninc3v  46455  omeiunltfirp  46490  hspdifhsp  46587  hspmbllem2  46598  pimdecfgtioo  46688  pimincfltioo  46689  preimageiingt  46691  preimaleiinlt  46692  smfid  46723  proththd  47588