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  8562  oewordri  8594  naddssim  8688  infxp  10285  lediv12a  12203  xmulgt0  13406  ioodisj  13606  leexp1a  14311  swrdswrdlem  14846  seqshft  15231  sumss2  15885  prmdvdsncoprmbd  16896  mulgfval  19272  grpissubg  19350  f1otrspeq  19654  mat1dimcrng  22785  matunitlindflem1  22987  matunitlindflem2  22988  elcls  23384  neiptopreu  23444  alexsubALTlem4  24362  ustuqtop2  24554  iscfil2  25580  absmuls  28623  tglowdim1i  28957  axcontlem2  29536  opreu2reuALT  33066  nsgqusf1olem1  33957  lbslelsp  34223  mh-inf3f1  37309  poimirlem4  38522  founiiun0  46174  xralrple2  46335  rexabslelem  46397  climisp  46725  climxrre  46729  cnrefiisplem  46808  sge0iunmptlemre  47394  nnfoctbdjlem  47434  iundjiun  47439  meaiuninc3v  47463  hoidmvlelem3  47576  hspmbllem2  47606  smflimlem2  47751