Metamath Proof Explorer


Theorem 3adantll2

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

Ref Expression
Hypothesis 3adantll2.1 φψχθτ
Assertion 3adantll2 φηψχθτ

Proof

Step Hyp Ref Expression
1 3adantll2.1 φψχθτ
2 simpll1 φηψχθφ
3 simpll3 φηψχθψ
4 2 3 jca φηψχθφψ
5 simplr φηψχθχ
6 simpr φηψχθθ
7 4 5 6 1 syl21anc φηψχθτ