Theorem ad4ant24 754

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 715	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓) → 𝜒)
3	2	adantlll 718	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:  oaass  8479  oewordri  8510  naddssim  8603  infxp  10108  lediv12a  12018  xmulgt0  13185  ioodisj  13385  leexp1a  14082  swrdswrdlem  14610  seqshft  14992  sumss2  15633  prmdvdsncoprmbd  16638  mulgfval  18948  grpissubg  19025  f1otrspeq  19326  mat1dimcrng  22362  elcls  22958  neiptopreu  23018  alexsubALTlem4  23935  ustuqtop2  24128  iscfil2  25164  absmuls  28151  tglowdim1i  28446  axcontlem2  28910  opreu2reuALT  32421  nsgqusf1olem1  33350  lbslelsp  33564  matunitlindflem1  37596  matunitlindflem2  37597  poimirlem4  37604  founiiun0  45168  xralrple2  45334  rexabslelem  45397  climisp  45727  climxrre  45731  cnrefiisplem  45810  sge0iunmptlemre  46396  nnfoctbdjlem  46436  iundjiun  46441  meaiuninc3v  46465  hoidmvlelem3  46578  hspmbllem2  46608  smflimlem2  46753