Theorem ad4ant24 755

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 716	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓) → 𝜒)
3	2	adantlll 719	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  8498  oewordri  8530  naddssim  8623  infxp  10136  lediv12a  12047  xmulgt0  13210  ioodisj  13410  leexp1a  14110  swrdswrdlem  14639  seqshft  15020  sumss2  15661  prmdvdsncoprmbd  16666  mulgfval  19011  grpissubg  19088  f1otrspeq  19388  mat1dimcrng  22433  elcls  23029  neiptopreu  23089  alexsubALTlem4  24006  ustuqtop2  24198  iscfil2  25234  absmuls  28252  tglowdim1i  28585  axcontlem2  29050  opreu2reuALT  32563  nsgqusf1olem1  33506  lbslelsp  33775  matunitlindflem1  37867  matunitlindflem2  37868  poimirlem4  37875  founiiun0  45549  xralrple2  45713  rexabslelem  45776  climisp  46104  climxrre  46108  cnrefiisplem  46187  sge0iunmptlemre  46773  nnfoctbdjlem  46813  iundjiun  46818  meaiuninc3v  46842  hoidmvlelem3  46955  hspmbllem2  46985  smflimlem2  47130