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  8488  oewordri  8520  naddssim  8613  infxp  10124  lediv12a  12035  xmulgt0  13198  ioodisj  13398  leexp1a  14098  swrdswrdlem  14627  seqshft  15008  sumss2  15649  prmdvdsncoprmbd  16654  mulgfval  18999  grpissubg  19076  f1otrspeq  19376  mat1dimcrng  22421  elcls  23017  neiptopreu  23077  alexsubALTlem4  23994  ustuqtop2  24186  iscfil2  25222  absmuls  28240  tglowdim1i  28573  axcontlem2  29038  opreu2reuALT  32551  nsgqusf1olem1  33494  lbslelsp  33754  matunitlindflem1  37817  matunitlindflem2  37818  poimirlem4  37825  founiiun0  45434  xralrple2  45599  rexabslelem  45662  climisp  45990  climxrre  45994  cnrefiisplem  46073  sge0iunmptlemre  46659  nnfoctbdjlem  46699  iundjiun  46704  meaiuninc3v  46728  hoidmvlelem3  46841  hspmbllem2  46871  smflimlem2  47016