This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )