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 397

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 398

This theorem is referenced by:  oaass  8561  oewordri  8592  naddssim  8684  infxp  10210  lediv12a  12107  xmulgt0  13262  ioodisj  13459  leexp1a  14140  swrdswrdlem  14654  seqshft  15032  sumss2  15672  prmdvdsncoprmbd  16663  mulgfval  18952  grpissubg  19026  f1otrspeq  19315  mat1dimcrng  21979  elcls  22577  neiptopreu  22637  alexsubALTlem4  23554  ustuqtop2  23747  iscfil2  24783  tglowdim1i  27752  axcontlem2  28223  opreu2reuALT  31717  nsgqusf1olem1  32524  matunitlindflem1  36484  matunitlindflem2  36485  poimirlem4  36492  founiiun0  43888  xralrple2  44064  rexabslelem  44128  climisp  44462  climxrre  44466  cnrefiisplem  44545  sge0iunmptlemre  45131  nnfoctbdjlem  45171  iundjiun  45176  meaiuninc3v  45200  hoidmvlelem3  45313  hspmbllem2  45343  smflimlem2  45488