Theorem ad4ant24 752

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  oaass  8189  oewordri  8220  infxp  9639  lediv12a  11535  xmulgt0  12679  ioodisj  12871  leexp1a  13542  swrdswrdlem  14068  seqshft  14446  sumss2  15085  mulgfval  18228  grpissubg  18301  f1otrspeq  18577  mat1dimcrng  21088  elcls  21683  neiptopreu  21743  alexsubALTlem4  22660  ustuqtop2  22853  iscfil2  23871  tglowdim1i  26289  axcontlem2  26753  opreu2reuALT  30242  matunitlindflem1  34890  matunitlindflem2  34891  founiiun0  41458  xralrple2  41629  rexabslelem  41699  climisp  42034  climxrre  42038  cnrefiisplem  42117  sge0iunmptlemre  42704  nnfoctbdjlem  42744  iundjiun  42749  meaiuninc3v  42773  hoidmvlelem3  42886  hspmbllem2  42916  smflimlem2  43055