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 396

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 206  df-an 397

This theorem is referenced by:  oaass  8563  oewordri  8594  naddssim  8686  infxp  10212  lediv12a  12109  xmulgt0  13264  ioodisj  13461  leexp1a  14142  swrdswrdlem  14656  seqshft  15034  sumss2  15674  prmdvdsncoprmbd  16665  mulgfval  18954  grpissubg  19028  f1otrspeq  19317  mat1dimcrng  21986  elcls  22584  neiptopreu  22644  alexsubALTlem4  23561  ustuqtop2  23754  iscfil2  24790  tglowdim1i  27790  axcontlem2  28261  opreu2reuALT  31755  nsgqusf1olem1  32569  matunitlindflem1  36570  matunitlindflem2  36571  poimirlem4  36578  founiiun0  43968  xralrple2  44143  rexabslelem  44207  climisp  44541  climxrre  44545  cnrefiisplem  44624  sge0iunmptlemre  45210  nnfoctbdjlem  45250  iundjiun  45255  meaiuninc3v  45279  hoidmvlelem3  45392  hspmbllem2  45422  smflimlem2  45567