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  8576  oewordri  8608  naddssim  8702  infxp  10299  lediv12a  12217  xmulgt0  13420  ioodisj  13620  leexp1a  14325  swrdswrdlem  14861  seqshft  15247  sumss2  15901  prmdvdsncoprmbd  16912  mulgfval  19288  grpissubg  19366  f1otrspeq  19670  mat1dimcrng  22801  matunitlindflem1  23003  matunitlindflem2  23004  elcls  23400  neiptopreu  23460  alexsubALTlem4  24378  ustuqtop2  24570  iscfil2  25596  absmuls  28639  tglowdim1i  28973  axcontlem2  29552  opreu2reuALT  33124  nsgqusf1olem1  34014  lbslelsp  34280  mh-inf3f1  37425  poimirlem4  38651  founiiun0  46313  xralrple2  46474  rexabslelem  46536  climisp  46864  climxrre  46868  cnrefiisplem  46947  sge0iunmptlemre  47533  nnfoctbdjlem  47573  iundjiun  47578  meaiuninc3v  47602  hoidmvlelem3  47715  hspmbllem2  47745  smflimlem2  47890