Theorem ad4ant24 755

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 716	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓) → 𝜒)
3	2	adantlll 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:  oaass  8496  oewordri  8528  naddssim  8621  infxp  10136  lediv12a  12049  xmulgt0  13235  ioodisj  13435  leexp1a  14137  swrdswrdlem  14666  seqshft  15047  sumss2  15688  prmdvdsncoprmbd  16697  mulgfval  19045  grpissubg  19122  f1otrspeq  19422  mat1dimcrng  22442  elcls  23038  neiptopreu  23098  alexsubALTlem4  24015  ustuqtop2  24207  iscfil2  25233  absmuls  28236  tglowdim1i  28569  axcontlem2  29034  opreu2reuALT  32546  nsgqusf1olem1  33473  lbslelsp  33742  matunitlindflem1  37937  matunitlindflem2  37938  poimirlem4  37945  founiiun0  45620  xralrple2  45784  rexabslelem  45846  climisp  46174  climxrre  46178  cnrefiisplem  46257  sge0iunmptlemre  46843  nnfoctbdjlem  46883  iundjiun  46888  meaiuninc3v  46912  hoidmvlelem3  47025  hspmbllem2  47055  smflimlem2  47200