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  8578  oewordri  8609  naddssim  8702  infxp  10233  lediv12a  12140  xmulgt0  13304  ioodisj  13504  leexp1a  14198  swrdswrdlem  14727  seqshft  15109  sumss2  15747  prmdvdsncoprmbd  16751  mulgfval  19057  grpissubg  19134  f1otrspeq  19433  mat1dimcrng  22420  elcls  23016  neiptopreu  23076  alexsubALTlem4  23993  ustuqtop2  24186  iscfil2  25223  absmuls  28203  tglowdim1i  28485  axcontlem2  28949  opreu2reuALT  32463  nsgqusf1olem1  33433  lbslelsp  33642  matunitlindflem1  37645  matunitlindflem2  37646  poimirlem4  37653  founiiun0  45181  xralrple2  45348  rexabslelem  45412  climisp  45742  climxrre  45746  cnrefiisplem  45825  sge0iunmptlemre  46411  nnfoctbdjlem  46451  iundjiun  46456  meaiuninc3v  46480  hoidmvlelem3  46593  hspmbllem2  46623  smflimlem2  46768