Metamath Proof Explorer


Theorem 3adantll3

Description: Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypothesis 3adantll3.1 ( ( ( ( 𝜑𝜓 ) ∧ 𝜒 ) ∧ 𝜃 ) → 𝜏 )
Assertion 3adantll3 ( ( ( ( 𝜑𝜓𝜂 ) ∧ 𝜒 ) ∧ 𝜃 ) → 𝜏 )

Proof

Step Hyp Ref Expression
1 3adantll3.1 ( ( ( ( 𝜑𝜓 ) ∧ 𝜒 ) ∧ 𝜃 ) → 𝜏 )
2 simpll1 ( ( ( ( 𝜑𝜓𝜂 ) ∧ 𝜒 ) ∧ 𝜃 ) → 𝜑 )
3 simpll2 ( ( ( ( 𝜑𝜓𝜂 ) ∧ 𝜒 ) ∧ 𝜃 ) → 𝜓 )
4 2 3 jca ( ( ( ( 𝜑𝜓𝜂 ) ∧ 𝜒 ) ∧ 𝜃 ) → ( 𝜑𝜓 ) )
5 simplr ( ( ( ( 𝜑𝜓𝜂 ) ∧ 𝜒 ) ∧ 𝜃 ) → 𝜒 )
6 simpr ( ( ( ( 𝜑𝜓𝜂 ) ∧ 𝜒 ) ∧ 𝜃 ) → 𝜃 )
7 4 5 6 1 syl21anc ( ( ( ( 𝜑𝜓𝜂 ) ∧ 𝜒 ) ∧ 𝜃 ) → 𝜏 )