Metamath Proof Explorer

Theorem bj-alrim

Description: Closed form of alrimi . (Contributed by BJ, 2-May-2019)

Ref Expression
Assertion bj-alrim 
|- ( F/ x ph -> ( A. x ( ph -> ps ) -> ( ph -> A. x ps ) ) )

Proof

Step Hyp Ref Expression
1 nf5r 
 |-  ( F/ x ph -> ( ph -> A. x ph ) )
2 sylgt 
 |-  ( A. x ( ph -> ps ) -> ( ( ph -> A. x ph ) -> ( ph -> A. x ps ) ) )
3 1 2 syl5com 
 |-  ( F/ x ph -> ( A. x ( ph -> ps ) -> ( ph -> A. x ps ) ) )