Theorem ad4ant24 767

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
ad4ant24	⊢ ((((𝜃 ∧ 𝜑) ∧ 𝜏) ∧ 𝜓) → 𝜒)

Proof of Theorem ad4ant24

Step	Hyp	Ref	Expression
1		ad4ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantlr 728	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓) → 𝜒)
3	2	adantlll 731	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:  oaass  8548  oewordri  8580  naddssim  8674  infxp  10216  lediv12a  12132  xmulgt0  13335  ioodisj  13535  leexp1a  14239  swrdswrdlem  14773  seqshft  15158  sumss2  15812  prmdvdsncoprmbd  16818  mulgfval  19192  grpissubg  19270  f1otrspeq  19574  mat1dimcrng  22699  matunitlindflem1  22901  matunitlindflem2  22902  elcls  23298  neiptopreu  23358  alexsubALTlem4  24276  ustuqtop2  24468  iscfil2  25494  absmuls  28509  tglowdim1i  28843  axcontlem2  29422  opreu2reuALT  32952  nsgqusf1olem1  33842  lbslelsp  34108  poimirlem4  38373  founiiun0  46022  xralrple2  46184  rexabslelem  46246  climisp  46574  climxrre  46578  cnrefiisplem  46657  sge0iunmptlemre  47243  nnfoctbdjlem  47283  iundjiun  47288  meaiuninc3v  47312  hoidmvlelem3  47425  hspmbllem2  47455  smflimlem2  47600