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  8525  oewordri  8556  naddssim  8649  infxp  10167  lediv12a  12076  xmulgt0  13243  ioodisj  13443  leexp1a  14140  swrdswrdlem  14669  seqshft  15051  sumss2  15692  prmdvdsncoprmbd  16697  mulgfval  19001  grpissubg  19078  f1otrspeq  19377  mat1dimcrng  22364  elcls  22960  neiptopreu  23020  alexsubALTlem4  23937  ustuqtop2  24130  iscfil2  25166  absmuls  28146  tglowdim1i  28428  axcontlem2  28892  opreu2reuALT  32406  nsgqusf1olem1  33384  lbslelsp  33593  matunitlindflem1  37610  matunitlindflem2  37611  poimirlem4  37618  founiiun0  45184  xralrple2  45350  rexabslelem  45414  climisp  45744  climxrre  45748  cnrefiisplem  45827  sge0iunmptlemre  46413  nnfoctbdjlem  46453  iundjiun  46458  meaiuninc3v  46482  hoidmvlelem3  46595  hspmbllem2  46625  smflimlem2  46770