Metamath Proof Explorer


Theorem adantl6r

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

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

Proof

Step Hyp Ref Expression
1 adantl6r.1 ( ( ( ( ( ( ( 𝜑𝜂 ) ∧ 𝜁 ) ∧ 𝜎 ) ∧ 𝜌 ) ∧ 𝜇 ) ∧ 𝜆 ) → 𝜅 )
2 1 ex ( ( ( ( ( ( 𝜑𝜂 ) ∧ 𝜁 ) ∧ 𝜎 ) ∧ 𝜌 ) ∧ 𝜇 ) → ( 𝜆𝜅 ) )
3 2 adantl5r ( ( ( ( ( ( ( 𝜑𝜏 ) ∧ 𝜂 ) ∧ 𝜁 ) ∧ 𝜎 ) ∧ 𝜌 ) ∧ 𝜇 ) → ( 𝜆𝜅 ) )
4 3 imp ( ( ( ( ( ( ( ( 𝜑𝜏 ) ∧ 𝜂 ) ∧ 𝜁 ) ∧ 𝜎 ) ∧ 𝜌 ) ∧ 𝜇 ) ∧ 𝜆 ) → 𝜅 )