Theorem ad4ant24 755

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 716	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓) → 𝜒)
3	2	adantlll 719	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  8487  oewordri  8519  naddssim  8612  infxp  10125  lediv12a  12038  xmulgt0  13224  ioodisj  13424  leexp1a  14126  swrdswrdlem  14655  seqshft  15036  sumss2  15677  prmdvdsncoprmbd  16686  mulgfval  19034  grpissubg  19111  f1otrspeq  19411  mat1dimcrng  22451  elcls  23047  neiptopreu  23107  alexsubALTlem4  24024  ustuqtop2  24216  iscfil2  25242  absmuls  28255  tglowdim1i  28588  axcontlem2  29053  opreu2reuALT  32566  nsgqusf1olem1  33493  lbslelsp  33762  matunitlindflem1  37948  matunitlindflem2  37949  poimirlem4  37956  founiiun0  45635  xralrple2  45799  rexabslelem  45861  climisp  46189  climxrre  46193  cnrefiisplem  46272  sge0iunmptlemre  46858  nnfoctbdjlem  46898  iundjiun  46903  meaiuninc3v  46927  hoidmvlelem3  47040  hspmbllem2  47070  smflimlem2  47215