Metamath Proof Explorer

Theorem bj-hbsb3t

Description: A theorem close to a closed form of hbsb3 . (Contributed by BJ, 2-May-2019)

Ref Expression
Assertion bj-hbsb3t 
|- ( A. x ( ph -> A. y ph ) -> ( [ y / x ] ph -> A. x [ y / x ] ph ) )

Proof

Step Hyp Ref Expression
1 spsbim 
 |-  ( A. x ( ph -> A. y ph ) -> ( [ y / x ] ph -> [ y / x ] A. y ph ) )
2 hbsb2a 
 |-  ( [ y / x ] A. y ph -> A. x [ y / x ] ph )
3 1 2 syl6 
 |-  ( A. x ( ph -> A. y ph ) -> ( [ y / x ] ph -> A. x [ y / x ] ph ) )