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 ψ