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  8502  oewordri  8533  naddssim  8626  infxp  10143  lediv12a  12052  xmulgt0  13219  ioodisj  13419  leexp1a  14116  swrdswrdlem  14645  seqshft  15027  sumss2  15668  prmdvdsncoprmbd  16673  mulgfval  18977  grpissubg  19054  f1otrspeq  19353  mat1dimcrng  22340  elcls  22936  neiptopreu  22996  alexsubALTlem4  23913  ustuqtop2  24106  iscfil2  25142  absmuls  28122  tglowdim1i  28404  axcontlem2  28868  opreu2reuALT  32379  nsgqusf1olem1  33357  lbslelsp  33566  matunitlindflem1  37583  matunitlindflem2  37584  poimirlem4  37591  founiiun0  45157  xralrple2  45323  rexabslelem  45387  climisp  45717  climxrre  45721  cnrefiisplem  45800  sge0iunmptlemre  46386  nnfoctbdjlem  46426  iundjiun  46431  meaiuninc3v  46455  hoidmvlelem3  46568  hspmbllem2  46598  smflimlem2  46743