Metamath Proof Explorer


Theorem 19.2d

Description: Deduction associated with 19.2 . (Contributed by BJ, 12-May-2019)

Ref Expression
Hypothesis 19.2d.1 φxψ
Assertion 19.2d φxψ

Proof

Step Hyp Ref Expression
1 19.2d.1 φxψ
2 19.2 xψxψ
3 1 2 syl φxψ