This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem adantlll

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004) (Proof shortened by Wolf Lammen, 2-Dec-2012)

Ref Expression
Hypothesis adantl2.1 ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) → 𝜃 )
Assertion adantlll ( ( ( ( 𝜏 ∧ 𝜑 ) ∧ 𝜓 ) ∧ 𝜒 ) → 𝜃 )

Proof

Step Hyp Ref Expression
1 adantl2.1 ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) → 𝜃 )
2 simpr ⊢ ( ( 𝜏 ∧ 𝜑 ) → 𝜑 )
3 2 1 sylanl1 ⊢ ( ( ( ( 𝜏 ∧ 𝜑 ) ∧ 𝜓 ) ∧ 𝜒 ) → 𝜃 )