Theorem ad4ant24 767

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 728	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓) → 𝜒)
3	2	adantlll 731	1 ⊢ ((((𝜃 ∧ 𝜑) ∧ 𝜏) ∧ 𝜓) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  oaass  8552  oewordri  8584  naddssim  8678  infxp  10213  lediv12a  12123  xmulgt0  13325  ioodisj  13525  leexp1a  14229  swrdswrdlem  14763  seqshft  15146  sumss2  15800  prmdvdsncoprmbd  16808  mulgfval  19179  grpissubg  19257  f1otrspeq  19561  mat1dimcrng  22684  elcls  23280  neiptopreu  23340  alexsubALTlem4  24258  ustuqtop2  24450  iscfil2  25476  absmuls  28488  tglowdim1i  28821  axcontlem2  29370  opreu2reuALT  32894  nsgqusf1olem1  33786  lbslelsp  34052  matunitlindflem1  38324  matunitlindflem2  38325  poimirlem4  38332  founiiun0  45966  xralrple2  46128  rexabslelem  46190  climisp  46518  climxrre  46522  cnrefiisplem  46601  sge0iunmptlemre  47187  nnfoctbdjlem  47227  iundjiun  47232  meaiuninc3v  47256  hoidmvlelem3  47369  hspmbllem2  47399  smflimlem2  47544