Theorem ad4ant24 753

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  oaass  8203  oewordri  8234  infxp  9688  lediv12a  11584  xmulgt0  12730  ioodisj  12927  leexp1a  13602  swrdswrdlem  14126  seqshft  14505  sumss2  15144  prmdvdsncoprmbd  16136  mulgfval  18307  grpissubg  18380  f1otrspeq  18656  mat1dimcrng  21191  elcls  21787  neiptopreu  21847  alexsubALTlem4  22764  ustuqtop2  22957  iscfil2  23980  tglowdim1i  26408  axcontlem2  26872  opreu2reuALT  30360  nsgqusf1olem1  31132  naddssim  33435  matunitlindflem1  35368  matunitlindflem2  35369  poimirlem4  35376  founiiun0  42232  xralrple2  42399  rexabslelem  42466  climisp  42799  climxrre  42803  cnrefiisplem  42882  sge0iunmptlemre  43465  nnfoctbdjlem  43505  iundjiun  43510  meaiuninc3v  43534  hoidmvlelem3  43647  hspmbllem2  43677  smflimlem2  43816