Theorem ad4ant24 754

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 715	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓) → 𝜒)
3	2	adantlll 718	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  8528  oewordri  8559  naddssim  8652  infxp  10174  lediv12a  12083  xmulgt0  13250  ioodisj  13450  leexp1a  14147  swrdswrdlem  14676  seqshft  15058  sumss2  15699  prmdvdsncoprmbd  16704  mulgfval  19008  grpissubg  19085  f1otrspeq  19384  mat1dimcrng  22371  elcls  22967  neiptopreu  23027  alexsubALTlem4  23944  ustuqtop2  24137  iscfil2  25173  absmuls  28153  tglowdim1i  28435  axcontlem2  28899  opreu2reuALT  32413  nsgqusf1olem1  33391  lbslelsp  33600  matunitlindflem1  37617  matunitlindflem2  37618  poimirlem4  37625  founiiun0  45191  xralrple2  45357  rexabslelem  45421  climisp  45751  climxrre  45755  cnrefiisplem  45834  sge0iunmptlemre  46420  nnfoctbdjlem  46460  iundjiun  46465  meaiuninc3v  46489  hoidmvlelem3  46602  hspmbllem2  46632  smflimlem2  46777