Theorem ad4ant24 766

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 727	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓) → 𝜒)
3	2	adantlll 730	1 ⊢ ((((𝜃 ∧ 𝜑) ∧ 𝜏) ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  oaass  8545  oewordri  8577  naddssim  8671  infxp  10196  lediv12a  12107  xmulgt0  13308  ioodisj  13508  leexp1a  14210  swrdswrdlem  14740  seqshft  15121  sumss2  15776  prmdvdsncoprmbd  16785  mulgfval  19134  grpissubg  19212  f1otrspeq  19516  mat1dimcrng  22602  elcls  23198  neiptopreu  23258  alexsubALTlem4  24175  ustuqtop2  24367  iscfil2  25393  absmuls  28402  tglowdim1i  28735  axcontlem2  29255  opreu2reuALT  32763  nsgqusf1olem1  33665  lbslelsp  33932  matunitlindflem1  38154  matunitlindflem2  38155  poimirlem4  38162  founiiun0  45799  xralrple2  45961  rexabslelem  46023  climisp  46351  climxrre  46355  cnrefiisplem  46434  sge0iunmptlemre  47020  nnfoctbdjlem  47060  iundjiun  47065  meaiuninc3v  47089  hoidmvlelem3  47202  hspmbllem2  47232  smflimlem2  47377