Metamath Proof Explorer


Theorem 3adantlr3

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

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

Proof

Step Hyp Ref Expression
1 3adantlr3.1 ( ( ( 𝜑 ∧ ( 𝜓𝜒 ) ) ∧ 𝜃 ) → 𝜏 )
2 simpll ( ( ( 𝜑 ∧ ( 𝜓𝜒𝜂 ) ) ∧ 𝜃 ) → 𝜑 )
3 simplr1 ( ( ( 𝜑 ∧ ( 𝜓𝜒𝜂 ) ) ∧ 𝜃 ) → 𝜓 )
4 simplr2 ( ( ( 𝜑 ∧ ( 𝜓𝜒𝜂 ) ) ∧ 𝜃 ) → 𝜒 )
5 3 4 jca ( ( ( 𝜑 ∧ ( 𝜓𝜒𝜂 ) ) ∧ 𝜃 ) → ( 𝜓𝜒 ) )
6 simpr ( ( ( 𝜑 ∧ ( 𝜓𝜒𝜂 ) ) ∧ 𝜃 ) → 𝜃 )
7 2 5 6 1 syl21anc ( ( ( 𝜑 ∧ ( 𝜓𝜒𝜂 ) ) ∧ 𝜃 ) → 𝜏 )