Metamath Proof Explorer

Theorem hbaltg

Description: A more general and closed form of hbal . (Contributed by Scott Fenton, 13-Dec-2010)

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

Proof

Step Hyp Ref Expression
1 alim 
 |-  ( A. x ( ph -> A. y ps ) -> ( A. x ph -> A. x A. y ps ) )
2 ax-11 
 |-  ( A. x A. y ps -> A. y A. x ps )
3 1 2 syl6 
 |-  ( A. x ( ph -> A. y ps ) -> ( A. x ph -> A. y A. x ps ) )