Theorem ad4ant24 764

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 725	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓) → 𝜒)
3	2	adantlll 728	1 ⊢ ((((𝜃 ∧ 𝜑) ∧ 𝜏) ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  oaass  8530  oewordri  8562  naddssim  8656  infxp  10170  lediv12a  12085  xmulgt0  13286  ioodisj  13486  leexp1a  14188  swrdswrdlem  14717  seqshft  15098  sumss2  15753  prmdvdsncoprmbd  16762  mulgfval  19111  grpissubg  19188  f1otrspeq  19487  mat1dimcrng  22534  elcls  23130  neiptopreu  23190  alexsubALTlem4  24107  ustuqtop2  24299  iscfil2  25325  absmuls  28334  tglowdim1i  28667  axcontlem2  29163  opreu2reuALT  32673  nsgqusf1olem1  33596  lbslelsp  33892  matunitlindflem1  38112  matunitlindflem2  38113  poimirlem4  38120  founiiun0  45765  xralrple2  45927  rexabslelem  45989  climisp  46317  climxrre  46321  cnrefiisplem  46400  sge0iunmptlemre  46986  nnfoctbdjlem  47026  iundjiun  47031  meaiuninc3v  47055  hoidmvlelem3  47168  hspmbllem2  47198  smflimlem2  47343