Metamath Proof Explorer

Theorem sbcim2gVD

Description: Distribution of class substitution over a left-nested implication. Similar to sbcimg . The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sbcim2g is sbcim2gVD without virtual deductions and was automatically derived from sbcim2gVD .

1:: |- (. A e. B ->. A e. B ).
2:: |- (. A e. B ,. [. A / x ]. ( ph -> ( ps -> ch ) ) ->. [. A / x ]. ( ph -> ( ps -> ch ) ) ).
3:1,2: |- (. A e. B ,. [. A / x ]. ( ph -> ( ps -> ch ) ) ->. ( [. A / x ]. ph -> [. A / x ]. ( ps -> ch ) ) ).
4:1: |- (. A e. B ->. ( [. A / x ]. ( ps -> ch ) <-> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ).
5:3,4: |- (. A e. B ,. [. A / x ]. ( ph -> ( ps -> ch ) ) ->. ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ).
6:5: |- (. A e. B ->. ( [. A / x ]. ( ph -> ( ps -> ch ) ) -> ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ) ).
7:: |- (. A e. B ,. ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ->. ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ).
8:4,7: |- (. A e. B ,. ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ->. ( [. A / x ]. ph -> [. A / x ]. ( ps -> ch ) ) ).
9:1: |- (. A e. B ->. ( [. A / x ]. ( ph -> ( ps -> ch ) ) <-> ( [. A / x ]. ph -> [. A / x ]. ( ps -> ch ) ) ) ).
10:8,9: |- (. A e. B ,. ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ->. [. A / x ]. ( ph -> ( ps -> ch ) ) ).
11:10: |- (. A e. B ->. ( ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) -> [. A / x ]. ( ph -> ( ps -> ch ) ) ) ).
12:6,11: |- (. A e. B ->. ( [. A / x ]. ( ph -> ( ps -> ch ) ) <-> ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ) ).
qed:12: |- ( A e. B -> ( [. A / x ]. ( ph -> ( ps -> ch ) ) <-> ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ) )
(Contributed by Alan Sare, 18-Mar-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sbcim2gVD 
|- ( A e. B -> ( [. A / x ]. ( ph -> ( ps -> ch ) ) <-> ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ) )

Proof

Step Hyp Ref Expression
1 idn1 
 |-  (. A e. B ->. A e. B ).
2 idn2 
 |-  (. A e. B ,. [. A / x ]. ( ph -> ( ps -> ch ) ) ->. [. A / x ]. ( ph -> ( ps -> ch ) ) ).
3 sbcimg 
 |-  ( A e. B -> ( [. A / x ]. ( ph -> ( ps -> ch ) ) <-> ( [. A / x ]. ph -> [. A / x ]. ( ps -> ch ) ) ) )
4 3 biimpd 
 |-  ( A e. B -> ( [. A / x ]. ( ph -> ( ps -> ch ) ) -> ( [. A / x ]. ph -> [. A / x ]. ( ps -> ch ) ) ) )
5 1 2 4 e12 
 |-  (. A e. B ,. [. A / x ]. ( ph -> ( ps -> ch ) ) ->. ( [. A / x ]. ph -> [. A / x ]. ( ps -> ch ) ) ).
6 sbcimg 
 |-  ( A e. B -> ( [. A / x ]. ( ps -> ch ) <-> ( [. A / x ]. ps -> [. A / x ]. ch ) ) )
7 1 6 e1a 
 |-  (. A e. B ->. ( [. A / x ]. ( ps -> ch ) <-> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ).
8 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 ) ) ) )
9 8 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 ) ) ) )
10 5 7 9 e21 
 |-  (. A e. B ,. [. A / x ]. ( ph -> ( ps -> ch ) ) ->. ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ).
11 10 in2 
 |-  (. A e. B ->. ( [. A / x ]. ( ph -> ( ps -> ch ) ) -> ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ) ).
12 idn2 
 |-  (. A e. B ,. ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ->. ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ).
13 biimpr 
 |-  ( ( [. A / x ]. ( ps -> ch ) <-> ( [. A / x ]. ps -> [. A / x ]. ch ) ) -> ( ( [. A / x ]. ps -> [. A / x ]. ch ) -> [. A / x ]. ( ps -> ch ) ) )
14 13 imim2d 
 |-  ( ( [. A / x ]. ( ps -> ch ) <-> ( [. A / x ]. ps -> [. A / x ]. ch ) ) -> ( ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) -> ( [. A / x ]. ph -> [. A / x ]. ( ps -> ch ) ) ) )
15 7 12 14 e12 
 |-  (. A e. B ,. ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ->. ( [. A / x ]. ph -> [. A / x ]. ( ps -> ch ) ) ).
16 1 3 e1a 
 |-  (. A e. B ->. ( [. A / x ]. ( ph -> ( ps -> ch ) ) <-> ( [. A / x ]. ph -> [. A / x ]. ( ps -> ch ) ) ) ).
17 biimpr 
 |-  ( ( [. A / x ]. ( ph -> ( ps -> ch ) ) <-> ( [. A / x ]. ph -> [. A / x ]. ( ps -> ch ) ) ) -> ( ( [. A / x ]. ph -> [. A / x ]. ( ps -> ch ) ) -> [. A / x ]. ( ph -> ( ps -> ch ) ) ) )
18 17 com12 
 |-  ( ( [. A / x ]. ph -> [. A / x ]. ( ps -> ch ) ) -> ( ( [. A / x ]. ( ph -> ( ps -> ch ) ) <-> ( [. A / x ]. ph -> [. A / x ]. ( ps -> ch ) ) ) -> [. A / x ]. ( ph -> ( ps -> ch ) ) ) )
19 15 16 18 e21 
 |-  (. A e. B ,. ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ->. [. A / x ]. ( ph -> ( ps -> ch ) ) ).
20 19 in2 
 |-  (. A e. B ->. ( ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) -> [. A / x ]. ( ph -> ( ps -> ch ) ) ) ).
21 impbi 
 |-  ( ( [. A / x ]. ( ph -> ( ps -> ch ) ) -> ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ) -> ( ( ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) -> [. A / x ]. ( ph -> ( ps -> ch ) ) ) -> ( [. A / x ]. ( ph -> ( ps -> ch ) ) <-> ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ) ) )
22 11 20 21 e11 
 |-  (. A e. B ->. ( [. A / x ]. ( ph -> ( ps -> ch ) ) <-> ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ) ).
23 22 in1 
 |-  ( A e. B -> ( [. A / x ]. ( ph -> ( ps -> ch ) ) <-> ( [. A / x ]. ph -> ( [. A / x ]. ps -> [. A / x ]. ch ) ) ) )