Theorem ad5antlr 736

Description: Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad5antlr	⊢ ((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Proof of Theorem ad5antlr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantl 481	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3	2	ad4antr 733	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:  simp-5r  786  fimaproj  8087  chnso  18559  restmetu  24526  foresf1o  32590  2ndresdju  32738  nn0xmulclb  32861  gsumwrd2dccatlem  33170  isdrng4  33388  fracfld  33401  elrspunidl  33520  elrspunsn  33521  rhmpreimaprmidl  33543  1arithidom  33629  mplvrpmga  33721  fedgmul  33808  locfinreflem  34017  pstmxmet  34074  satfdmlem  35581  mblfinlem3  37904  itg2gt0cn  37920  dffltz  42986  pell1234qrmulcl  43206  suplesup  45692  limclner  46003  bgoldbtbnd  48163  gricushgr  48271