Metamath Proof Explorer

Theorem sbcbi

Description: Implication form of sbcbii . sbcbi is sbcbiVD without virtual deductions and was automatically derived from sbcbiVD using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	sbcbi	\|- ( A e. V -> ( A. x ( ph <-> ps ) -> ( [. A / x ]. ph <-> [. A / x ]. ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		spsbc	\|- ( A e. V -> ( A. x ( ph <-> ps ) -> [. A / x ]. ( ph <-> ps ) ) )
2		sbcbig	\|- ( A e. V -> ( [. A / x ]. ( ph <-> ps ) <-> ( [. A / x ]. ph <-> [. A / x ]. ps ) ) )
3	1 2	sylibd	\|- ( A e. V -> ( A. x ( ph <-> ps ) -> ( [. A / x ]. ph <-> [. A / x ]. ps ) ) )

Step

Hyp

Ref

Expression

spsbc

 |-  ( A e. V -> ( A. x ( ph <-> ps ) -> [. A / x ]. ( ph <-> ps ) ) )

sbcbig

 |-  ( A e. V -> ( [. A / x ]. ( ph <-> ps ) <-> ( [. A / x ]. ph <-> [. A / x ]. ps ) ) )

1 2

sylibd

 |-  ( A e. V -> ( A. x ( ph <-> ps ) -> ( [. A / x ]. ph <-> [. A / x ]. ps ) ) )