Theorem ad4ant24 751

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 712	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓) → 𝜒)
3	2	adantlll 715	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  8567  oewordri  8598  naddssim  8690  infxp  10216  lediv12a  12114  xmulgt0  13269  ioodisj  13466  leexp1a  14147  swrdswrdlem  14661  seqshft  15039  sumss2  15679  prmdvdsncoprmbd  16670  mulgfval  18995  grpissubg  19069  f1otrspeq  19363  mat1dimcrng  22298  elcls  22896  neiptopreu  22956  alexsubALTlem4  23873  ustuqtop2  24066  iscfil2  25113  absmuls  28050  tglowdim1i  28184  axcontlem2  28655  opreu2reuALT  32149  nsgqusf1olem1  32963  matunitlindflem1  36947  matunitlindflem2  36948  poimirlem4  36955  founiiun0  44347  xralrple2  44522  rexabslelem  44586  climisp  44920  climxrre  44924  cnrefiisplem  45003  sge0iunmptlemre  45589  nnfoctbdjlem  45629  iundjiun  45634  meaiuninc3v  45658  hoidmvlelem3  45771  hspmbllem2  45801  smflimlem2  45946