Metamath Proof Explorer

Theorem bj-hbalt

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

Ref Expression
Assertion bj-hbalt 
|- ( A. y ( ph -> A. x ps ) -> ( A. y ph -> A. x A. y ps ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A. y ( ph -> A. x ps ) -> A. y ( ph -> A. x ps ) )
2 id 
 |-  ( ( ph -> A. x ps ) -> ( ph -> A. x ps ) )
3 1 2 bj-hbald 
 |-  ( A. y ( ph -> A. x ps ) -> ( A. y ph -> A. x A. y ps ) )