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