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 φ ψ η χ θ τ