Metamath Proof Explorer

Theorem sbcbi2OLD

Description: Obsolete proof of sbcbi2 as of 5-May-2024. (Contributed by Giovanni Mascellani, 9-Apr-2018) (Proof shortened by Wolf Lammen, 4-May-2023) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 nfa1 
 |-  F/ x A. x ( ph <-> ps )
2 sp 
 |-  ( A. x ( ph <-> ps ) -> ( ph <-> ps ) )
3 1 2 sbcbid 
 |-  ( A. x ( ph <-> ps ) -> ( [. A / x ]. ph <-> [. A / x ]. ps ) )