This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 19.2d

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

Ref Expression
Hypothesis 19.2d.1 
|- ( ph -> A. x ps )
Assertion 19.2d 
|- ( ph -> E. x ps )

Proof

Step Hyp Ref Expression
1 19.2d.1 
 |-  ( ph -> A. x ps )
2 19.2 
 |-  ( A. x ps -> E. x ps )
3 1 2 syl 
 |-  ( ph -> E. x ps )