Metamath Proof Explorer


Theorem adantl3r

Description: Deduction adding 1 conjunct to antecedent. (Contributed by Alan Sare, 17-Oct-2017)

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

Proof

Step Hyp Ref Expression
1 adantl3r.1 φψχθτ
2 id φψφψ
3 2 adantlr φηψφψ
4 3 1 sylanl1 φηψχθτ