Theorem adantl6r 776

Description: Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.)

Hypothesis

Ref	Expression
adantl6r.1	⊢ (((((((𝜑 ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅)

Assertion

Ref	Expression
adantl6r	⊢ ((((((((𝜑 ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅)

Proof of Theorem adantl6r

Step	Hyp	Ref	Expression
1		adantl6r.1	. . . 4 ⊢ (((((((𝜑 ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅)
2	1	ex 418	. . 3 ⊢ ((((((𝜑 ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → (𝜆 → 𝜅))
3	2	adantl5r 775	. 2 ⊢ (((((((𝜑 ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → (𝜆 → 𝜅))
4	3	imp 412	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:  pstmxmet  34353