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  8476  oewordri  8507  naddssim  8600  infxp  10105  lediv12a  12015  xmulgt0  13182  ioodisj  13382  leexp1a  14082  swrdswrdlem  14611  seqshft  14992  sumss2  15633  prmdvdsncoprmbd  16638  mulgfval  18982  grpissubg  19059  f1otrspeq  19359  mat1dimcrng  22392  elcls  22988  neiptopreu  23048  alexsubALTlem4  23965  ustuqtop2  24157  iscfil2  25193  absmuls  28182  tglowdim1i  28479  axcontlem2  28943  opreu2reuALT  32456  nsgqusf1olem1  33378  lbslelsp  33610  matunitlindflem1  37664  matunitlindflem2  37665  poimirlem4  37672  founiiun0  45235  xralrple2  45401  rexabslelem  45464  climisp  45792  climxrre  45796  cnrefiisplem  45875  sge0iunmptlemre  46461  nnfoctbdjlem  46501  iundjiun  46506  meaiuninc3v  46530  hoidmvlelem3  46643  hspmbllem2  46673  smflimlem2  46818