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  8570  oewordri  8602  naddssim  8696  infxp  10293  lediv12a  12211  xmulgt0  13414  ioodisj  13614  leexp1a  14319  swrdswrdlem  14854  seqshft  15239  sumss2  15893  prmdvdsncoprmbd  16904  mulgfval  19280  grpissubg  19358  f1otrspeq  19662  mat1dimcrng  22793  matunitlindflem1  22995  matunitlindflem2  22996  elcls  23392  neiptopreu  23452  alexsubALTlem4  24370  ustuqtop2  24562  iscfil2  25588  absmuls  28631  tglowdim1i  28965  axcontlem2  29544  opreu2reuALT  33116  nsgqusf1olem1  34007  lbslelsp  34273  mh-inf3f1  37404  poimirlem4  38618  founiiun0  46281  xralrple2  46442  rexabslelem  46504  climisp  46832  climxrre  46836  cnrefiisplem  46915  sge0iunmptlemre  47501  nnfoctbdjlem  47541  iundjiun  47546  meaiuninc3v  47570  hoidmvlelem3  47683  hspmbllem2  47713  smflimlem2  47858