Metamath Proof Explorer


Theorem sbcim2g

Description: Distribution of class substitution over a left-nested implication. Similar to sbcimg . sbcim2g is sbcim2gVD without virtual deductions and was automatically derived from sbcim2gVD 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 sbcim2g
|- ( A e. V -> ( [. A / x ]. ( ph -> ( ps -> ch ) ) <-> ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ) )

Proof

Step Hyp Ref Expression
1 sbcimg
 |-  ( A e. V -> ( [. A / x ]. ( ph -> ( ps -> ch ) ) <-> ( [. A / x ]. ph -> [. A / x ]. ( ps -> ch ) ) ) )
2 1 biimpd
 |-  ( A e. V -> ( [. A / x ]. ( ph -> ( ps -> ch ) ) -> ( [. A / x ]. ph -> [. A / x ]. ( ps -> ch ) ) ) )
3 sbcimg
 |-  ( A e. V -> ( [. A / x ]. ( ps -> ch ) <-> ( [. A / x ]. ps -> [. A / x ]. ch ) ) )
4 imbi2
 |-  ( ( [. A / x ]. ( ps -> ch ) <-> ( [. A / x ]. ps -> [. A / x ]. ch ) ) -> ( ( [. A / x ]. ph -> [. A / x ]. ( ps -> ch ) ) <-> ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ) )
5 4 biimpcd
 |-  ( ( [. A / x ]. ph -> [. A / x ]. ( ps -> ch ) ) -> ( ( [. A / x ]. ( ps -> ch ) <-> ( [. A / x ]. ps -> [. A / x ]. ch ) ) -> ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ) )
6 2 3 5 syl6ci
 |-  ( A e. V -> ( [. A / x ]. ( ph -> ( ps -> ch ) ) -> ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ) )
7 idd
 |-  ( A e. V -> ( ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) -> ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ) )
8 biimpr
 |-  ( ( [. A / x ]. ( ps -> ch ) <-> ( [. A / x ]. ps -> [. A / x ]. ch ) ) -> ( ( [. A / x ]. ps -> [. A / x ]. ch ) -> [. A / x ]. ( ps -> ch ) ) )
9 3 7 8 ee13
 |-  ( A e. V -> ( ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) -> ( [. A / x ]. ph -> [. A / x ]. ( ps -> ch ) ) ) )
10 9 1 sylibrd
 |-  ( A e. V -> ( ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) -> [. A / x ]. ( ph -> ( ps -> ch ) ) ) )
11 6 10 impbid
 |-  ( A e. V -> ( [. A / x ]. ( ph -> ( ps -> ch ) ) <-> ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ) )