Metamath Proof Explorer


Theorem spsbbi

Description: Biconditional property for substitution. Closed form of sbbii . Specialization of biconditional. (Contributed by NM, 2-Jun-1993) Revise df-sb . (Revised by BJ, 22-Dec-2020)

Ref Expression
Assertion spsbbi
|- ( A. x ( ph <-> ps ) -> ( [ t / x ] ph <-> [ t / x ] ps ) )

Proof

Step Hyp Ref Expression
1 biimp
 |-  ( ( ph <-> ps ) -> ( ph -> ps ) )
2 1 alimi
 |-  ( A. x ( ph <-> ps ) -> A. x ( ph -> ps ) )
3 spsbim
 |-  ( A. x ( ph -> ps ) -> ( [ t / x ] ph -> [ t / x ] ps ) )
4 2 3 syl
 |-  ( A. x ( ph <-> ps ) -> ( [ t / x ] ph -> [ t / x ] ps ) )
5 biimpr
 |-  ( ( ph <-> ps ) -> ( ps -> ph ) )
6 5 alimi
 |-  ( A. x ( ph <-> ps ) -> A. x ( ps -> ph ) )
7 spsbim
 |-  ( A. x ( ps -> ph ) -> ( [ t / x ] ps -> [ t / x ] ph ) )
8 6 7 syl
 |-  ( A. x ( ph <-> ps ) -> ( [ t / x ] ps -> [ t / x ] ph ) )
9 4 8 impbid
 |-  ( A. x ( ph <-> ps ) -> ( [ t / x ] ph <-> [ t / x ] ps ) )