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 395

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 207  df-an 396

This theorem is referenced by:  oaass  8617  oewordri  8648  naddssim  8741  infxp  10283  lediv12a  12188  xmulgt0  13345  ioodisj  13542  leexp1a  14225  swrdswrdlem  14752  seqshft  15134  sumss2  15774  prmdvdsncoprmbd  16774  mulgfval  19109  grpissubg  19186  f1otrspeq  19489  mat1dimcrng  22504  elcls  23102  neiptopreu  23162  alexsubALTlem4  24079  ustuqtop2  24272  iscfil2  25319  absmuls  28286  tglowdim1i  28527  axcontlem2  28998  opreu2reuALT  32505  nsgqusf1olem1  33406  matunitlindflem1  37576  matunitlindflem2  37577  poimirlem4  37584  founiiun0  45097  xralrple2  45269  rexabslelem  45333  climisp  45667  climxrre  45671  cnrefiisplem  45750  sge0iunmptlemre  46336  nnfoctbdjlem  46376  iundjiun  46381  meaiuninc3v  46405  hoidmvlelem3  46518  hspmbllem2  46548  smflimlem2  46693