Theorem ad5antlr 733

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 484	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3	2	ad4antr 730	1 ⊢ ((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  simp-5r  784  fimaproj  7831  restmetu  23182  foresf1o  30267  nn0xmulclb  30498  fedgmul  31029  locfinreflem  31106  pstmxmet  31139  satfdmlem  32617  mblfinlem3  34933  itg2gt0cn  34949  dffltz  39278  pell1234qrmulcl  39459  suplesup  41614  limclner  41939  bgoldbtbnd  43981  isomushgr  43998