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  8490  oewordri  8522  naddssim  8615  infxp  10130  lediv12a  12043  xmulgt0  13229  ioodisj  13429  leexp1a  14131  swrdswrdlem  14660  seqshft  15041  sumss2  15682  prmdvdsncoprmbd  16691  mulgfval  19039  grpissubg  19116  f1otrspeq  19416  mat1dimcrng  22455  elcls  23051  neiptopreu  23111  alexsubALTlem4  24028  ustuqtop2  24220  iscfil2  25246  absmuls  28253  tglowdim1i  28586  axcontlem2  29051  opreu2reuALT  32564  nsgqusf1olem1  33491  lbslelsp  33760  matunitlindflem1  37954  matunitlindflem2  37955  poimirlem4  37962  founiiun0  45641  xralrple2  45805  rexabslelem  45867  climisp  46195  climxrre  46199  cnrefiisplem  46278  sge0iunmptlemre  46864  nnfoctbdjlem  46904  iundjiun  46909  meaiuninc3v  46933  hoidmvlelem3  47046  hspmbllem2  47076  smflimlem2  47221