Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > 2pm13.193VD | Structured version Visualization version Unicode version |
Description: Virtual deduction proof of 2pm13.193 38768.
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.
2pm13.193 38768 is 2pm13.193VD 39139 without virtual deductions and was
automatically derived from 2pm13.193VD 39139. (Contributed by Alan Sare,
8-Feb-2014.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
Ref | Expression |
---|---|
2pm13.193VD |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idn1 38790 | . . . . 5 | |
2 | simpl 473 | . . . . 5 | |
3 | 1, 2 | e1a 38852 | . . . 4 |
4 | simpl 473 | . . . . . . . . . . 11 | |
5 | 3, 4 | e1a 38852 | . . . . . . . . . 10 |
6 | simpr 477 | . . . . . . . . . . 11 | |
7 | 1, 6 | e1a 38852 | . . . . . . . . . 10 |
8 | pm3.21 464 | . . . . . . . . . 10 | |
9 | 5, 7, 8 | e11 38913 | . . . . . . . . 9 |
10 | sbequ2 1882 | . . . . . . . . . 10 | |
11 | 10 | imdistanri 727 | . . . . . . . . 9 |
12 | 9, 11 | e1a 38852 | . . . . . . . 8 |
13 | simpl 473 | . . . . . . . 8 | |
14 | 12, 13 | e1a 38852 | . . . . . . 7 |
15 | simpr 477 | . . . . . . . 8 | |
16 | 3, 15 | e1a 38852 | . . . . . . 7 |
17 | pm3.2 463 | . . . . . . 7 | |
18 | 14, 16, 17 | e11 38913 | . . . . . 6 |
19 | sbequ2 1882 | . . . . . . 7 | |
20 | 19 | imdistanri 727 | . . . . . 6 |
21 | 18, 20 | e1a 38852 | . . . . 5 |
22 | simpl 473 | . . . . 5 | |
23 | 21, 22 | e1a 38852 | . . . 4 |
24 | pm3.2 463 | . . . 4 | |
25 | 3, 23, 24 | e11 38913 | . . 3 |
26 | 25 | in1 38787 | . 2 |
27 | idn1 38790 | . . . . 5 | |
28 | simpl 473 | . . . . 5 | |
29 | 27, 28 | e1a 38852 | . . . 4 |
30 | 29, 4 | e1a 38852 | . . . . . . 7 |
31 | 29, 15 | e1a 38852 | . . . . . . . . . 10 |
32 | simpr 477 | . . . . . . . . . . 11 | |
33 | 27, 32 | e1a 38852 | . . . . . . . . . 10 |
34 | pm3.21 464 | . . . . . . . . . 10 | |
35 | 31, 33, 34 | e11 38913 | . . . . . . . . 9 |
36 | sbequ1 2110 | . . . . . . . . . 10 | |
37 | 36 | imdistanri 727 | . . . . . . . . 9 |
38 | 35, 37 | e1a 38852 | . . . . . . . 8 |
39 | simpl 473 | . . . . . . . 8 | |
40 | 38, 39 | e1a 38852 | . . . . . . 7 |
41 | pm3.21 464 | . . . . . . 7 | |
42 | 30, 40, 41 | e11 38913 | . . . . . 6 |
43 | sbequ1 2110 | . . . . . . 7 | |
44 | 43 | imdistanri 727 | . . . . . 6 |
45 | 42, 44 | e1a 38852 | . . . . 5 |
46 | simpl 473 | . . . . 5 | |
47 | 45, 46 | e1a 38852 | . . . 4 |
48 | pm3.2 463 | . . . 4 | |
49 | 29, 47, 48 | e11 38913 | . . 3 |
50 | 49 | in1 38787 | . 2 |
51 | 26, 50 | impbii 199 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 196 wa 384 wceq 1483 wsb 1880 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-12 2047 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-sb 1881 df-vd1 38786 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |