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  8542  oewordri  8574  naddssim  8668  infxp  10193  lediv12a  12103  xmulgt0  13304  ioodisj  13504  leexp1a  14207  swrdswrdlem  14737  seqshft  15118  sumss2  15773  prmdvdsncoprmbd  16781  mulgfval  19130  grpissubg  19208  f1otrspeq  19512  mat1dimcrng  22634  elcls  23230  neiptopreu  23290  alexsubALTlem4  24207  ustuqtop2  24399  iscfil2  25425  absmuls  28437  tglowdim1i  28770  axcontlem2  29315  opreu2reuALT  32823  nsgqusf1olem1  33722  lbslelsp  33988  matunitlindflem1  38267  matunitlindflem2  38268  poimirlem4  38275  founiiun0  45908  xralrple2  46070  rexabslelem  46132  climisp  46460  climxrre  46464  cnrefiisplem  46543  sge0iunmptlemre  47129  nnfoctbdjlem  47169  iundjiun  47174  meaiuninc3v  47198  hoidmvlelem3  47311  hspmbllem2  47341  smflimlem2  47486