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 396

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 397

This theorem is referenced by:  oaass  8392  oewordri  8423  infxp  9971  lediv12a  11868  xmulgt0  13017  ioodisj  13214  leexp1a  13893  swrdswrdlem  14417  seqshft  14796  sumss2  15438  prmdvdsncoprmbd  16431  mulgfval  18702  grpissubg  18775  f1otrspeq  19055  mat1dimcrng  21626  elcls  22224  neiptopreu  22284  alexsubALTlem4  23201  ustuqtop2  23394  iscfil2  24430  tglowdim1i  26862  axcontlem2  27333  opreu2reuALT  30825  nsgqusf1olem1  31598  naddssim  33837  matunitlindflem1  35773  matunitlindflem2  35774  poimirlem4  35781  founiiun0  42728  xralrple2  42893  rexabslelem  42958  climisp  43287  climxrre  43291  cnrefiisplem  43370  sge0iunmptlemre  43953  nnfoctbdjlem  43993  iundjiun  43998  meaiuninc3v  44022  hoidmvlelem3  44135  hspmbllem2  44165  smflimlem2  44307