Theorem ad4ant24 767

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  oaass  8607  oewordri  8639  naddssim  8733  infxp  10331  lediv12a  12250  xmulgt0  13453  ioodisj  13653  leexp1a  14358  swrdswrdlem  14895  seqshft  15281  sumss2  15936  prmdvdsncoprmbd  16947  mulgfval  19329  grpissubg  19407  f1otrspeq  19712  mat1dimcrng  22847  matunitlindflem1  23049  matunitlindflem2  23050  elcls  23446  neiptopreu  23506  alexsubALTlem4  24424  ustuqtop2  24616  iscfil2  25642  absmuls  28687  tglowdim1i  29021  axcontlem2  29600  opreu2reuALT  33172  nsgqusf1olem1  34068  lbslelsp  34341  mh-inf3f1  37544  poimirlem4  38810  founiiun0  46478  xralrple2  46639  rexabslelem  46701  climisp  47029  climxrre  47033  cnrefiisplem  47112  sge0iunmptlemre  47698  nnfoctbdjlem  47738  iundjiun  47743  meaiuninc3v  47767  hoidmvlelem3  47880  hspmbllem2  47910  smflimlem2  48055