Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sbcim2gVD Unicode version

Theorem sbcim2gVD 28396
Description: Distribution of class substitution over a left-nested implication. Similar to sbcimg 3108. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sbcim2g 28030 is sbcim2gVD 28396 without virtual deductions and was automatically derived from sbcim2gVD 28396.
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.)
Assertion
Ref Expression
sbcim2gVD  |-  ( A  e.  B  ->  ( [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  <-> 
( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ) )

Proof of Theorem sbcim2gVD
StepHypRef Expression
1 idn1 28070 . . . . . 6  |-  (. A  e.  B  ->.  A  e.  B ).
2 idn2 28119 . . . . . 6  |-  (. A  e.  B ,. [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  ->.  [. A  /  x ]. ( ph  ->  ( ps  ->  ch )
) ).
3 sbcimg 3108 . . . . . . 7  |-  ( A  e.  B  ->  ( [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  <-> 
( [. A  /  x ]. ph  ->  [. A  /  x ]. ( ps  ->  ch ) ) ) )
43biimpd 198 . . . . . 6  |-  ( A  e.  B  ->  ( [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  ->  ( [. A  /  x ]. ph  ->  [. A  /  x ]. ( ps  ->  ch )
) ) )
51, 2, 4e12 28242 . . . . 5  |-  (. A  e.  B ,. [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  ->.  ( [. A  /  x ]. ph  ->  [. A  /  x ]. ( ps  ->  ch )
) ).
6 sbcimg 3108 . . . . . 6  |-  ( A  e.  B  ->  ( [. A  /  x ]. ( ps  ->  ch ) 
<->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch )
) )
71, 6e1_ 28133 . . . . 5  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ps 
->  ch )  <->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ).
8 imbi2 314 . . . . . 6  |-  ( (
[. 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 ) ) ) )
98biimpcd 215 . . . . 5  |-  ( (
[. 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 ) ) ) )
105, 7, 9e21 28248 . . . 4  |-  (. A  e.  B ,. [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  ->.  ( [. A  /  x ]. ph  ->  (
[. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ).
1110in2 28111 . . 3  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  ->  ( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ) ).
12 idn2 28119 . . . . . 6  |-  (. A  e.  B ,. ( [. A  /  x ]. ph  ->  (
[. A  /  x ]. ps  ->  [. A  /  x ]. ch ) )  ->.  ( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ).
13 bi2 189 . . . . . . 7  |-  ( (
[. A  /  x ]. ( ps  ->  ch ) 
<->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch )
)  ->  ( ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch )  ->  [. A  /  x ]. ( ps  ->  ch ) ) )
1413imim2d 48 . . . . . 6  |-  ( (
[. 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 ) ) ) )
157, 12, 14e12 28242 . . . . 5  |-  (. A  e.  B ,. ( [. A  /  x ]. ph  ->  (
[. A  /  x ]. ps  ->  [. A  /  x ]. ch ) )  ->.  ( [. A  /  x ]. ph  ->  [. A  /  x ]. ( ps  ->  ch ) ) ).
161, 3e1_ 28133 . . . . 5  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  <->  ( [. A  /  x ]. ph  ->  [. A  /  x ]. ( ps  ->  ch )
) ) ).
17 bi2 189 . . . . . 6  |-  ( (
[. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  <-> 
( [. A  /  x ]. ph  ->  [. A  /  x ]. ( ps  ->  ch ) ) )  -> 
( ( [. A  /  x ]. ph  ->  [. A  /  x ]. ( ps  ->  ch )
)  ->  [. A  /  x ]. ( ph  ->  ( ps  ->  ch )
) ) )
1817com12 27 . . . . 5  |-  ( (
[. A  /  x ]. ph  ->  [. A  /  x ]. ( ps  ->  ch ) )  ->  (
( [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  <-> 
( [. A  /  x ]. ph  ->  [. A  /  x ]. ( ps  ->  ch ) ) )  ->  [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) ) ) )
1915, 16, 18e21 28248 . . . 4  |-  (. A  e.  B ,. ( [. A  /  x ]. ph  ->  (
[. A  /  x ]. ps  ->  [. A  /  x ]. ch ) )  ->.  [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) ) ).
2019in2 28111 . . 3  |-  (. A  e.  B  ->.  ( ( [. A  /  x ]. ph  ->  (
[. A  /  x ]. ps  ->  [. A  /  x ]. ch ) )  ->  [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) ) ) ).
21 bi3 179 . . 3  |-  ( (
[. 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 ) ) ) ) )
2211, 20, 21e11 28194 . 2  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  <->  ( [. A  /  x ]. ph  ->  (
[. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ) ).
2322in1 28067 1  |-  ( A  e.  B  ->  ( [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  <-> 
( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    e. wcel 1710   [.wsbc 3067
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-v 2866  df-sbc 3068  df-vd1 28066  df-vd2 28075
  Copyright terms: Public domain W3C validator