Theorem ad4ant24 750

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 711	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓) → 𝜒)
3	2	adantlll 714	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 206  df-an 396

This theorem is referenced by:  oaass  8354  oewordri  8385  infxp  9902  lediv12a  11798  xmulgt0  12946  ioodisj  13143  leexp1a  13821  swrdswrdlem  14345  seqshft  14724  sumss2  15366  prmdvdsncoprmbd  16359  mulgfval  18617  grpissubg  18690  f1otrspeq  18970  mat1dimcrng  21534  elcls  22132  neiptopreu  22192  alexsubALTlem4  23109  ustuqtop2  23302  iscfil2  24335  tglowdim1i  26766  axcontlem2  27236  opreu2reuALT  30726  nsgqusf1olem1  31500  naddssim  33764  matunitlindflem1  35700  matunitlindflem2  35701  poimirlem4  35708  founiiun0  42617  xralrple2  42783  rexabslelem  42848  climisp  43177  climxrre  43181  cnrefiisplem  43260  sge0iunmptlemre  43843  nnfoctbdjlem  43883  iundjiun  43888  meaiuninc3v  43912  hoidmvlelem3  44025  hspmbllem2  44055  smflimlem2  44194