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

Theorem sbcim2gVD 37266
Description: Distribution of class substitution over a left-nested implication. Similar to sbcimg 3308. 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 36893 is sbcim2gVD 37266 without virtual deductions and was automatically derived from sbcim2gVD 37266.
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 36938 . . . . . 6  |-  (. A  e.  B  ->.  A  e.  B ).
2 idn2 36986 . . . . . 6  |-  (. A  e.  B ,. [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  ->.  [. A  /  x ]. ( ph  ->  ( ps  ->  ch )
) ).
3 sbcimg 3308 . . . . . . 7  |-  ( A  e.  B  ->  ( [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  <-> 
( [. A  /  x ]. ph  ->  [. A  /  x ]. ( ps  ->  ch ) ) ) )
43biimpd 211 . . . . . 6  |-  ( A  e.  B  ->  ( [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  ->  ( [. A  /  x ]. ph  ->  [. A  /  x ]. ( ps  ->  ch )
) ) )
51, 2, 4e12 37105 . . . . 5  |-  (. A  e.  B ,. [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  ->.  ( [. A  /  x ]. ph  ->  [. A  /  x ]. ( ps  ->  ch )
) ).
6 sbcimg 3308 . . . . . 6  |-  ( A  e.  B  ->  ( [. A  /  x ]. ( ps  ->  ch ) 
<->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch )
) )
71, 6e1a 37000 . . . . 5  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ps 
->  ch )  <->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ).
8 imbi2 326 . . . . . 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 228 . . . . 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 37111 . . . 4  |-  (. A  e.  B ,. [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  ->.  ( [. A  /  x ]. ph  ->  (
[. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ).
1110in2 36978 . . 3  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  ->  ( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ) ).
12 idn2 36986 . . . . . 6  |-  (. A  e.  B ,. ( [. A  /  x ]. ph  ->  (
[. A  /  x ]. ps  ->  [. A  /  x ]. ch ) )  ->.  ( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ).
13 biimpr 202 . . . . . . 7  |-  ( (
[. A  /  x ]. ( ps  ->  ch ) 
<->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch )
)  ->  ( ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch )  ->  [. A  /  x ]. ( ps  ->  ch ) ) )
1413imim2d 54 . . . . . 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 37105 . . . . 5  |-  (. A  e.  B ,. ( [. A  /  x ]. ph  ->  (
[. A  /  x ]. ps  ->  [. A  /  x ]. ch ) )  ->.  ( [. A  /  x ]. ph  ->  [. A  /  x ]. ( ps  ->  ch ) ) ).
161, 3e1a 37000 . . . . 5  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  <->  ( [. A  /  x ]. ph  ->  [. A  /  x ]. ( ps  ->  ch )
) ) ).
17 biimpr 202 . . . . . 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 32 . . . . 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 37111 . . . 4  |-  (. A  e.  B ,. ( [. A  /  x ]. ph  ->  (
[. A  /  x ]. ps  ->  [. A  /  x ]. ch ) )  ->.  [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) ) ).
2019in2 36978 . . 3  |-  (. A  e.  B  ->.  ( ( [. A  /  x ]. ph  ->  (
[. A  /  x ]. ps  ->  [. A  /  x ]. ch ) )  ->  [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) ) ) ).
21 impbi 190 . . 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 37061 . 2  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  <->  ( [. A  /  x ]. ph  ->  (
[. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ) ).
2322in1 36935 1  |-  ( A  e.  B  ->  ( [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  <-> 
( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    e. wcel 1886   [.wsbc 3266
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-12 1932  ax-13 2090  ax-ext 2430
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-v 3046  df-sbc 3267  df-vd1 36934  df-vd2 36942
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator