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