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