Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > suctrALTcfVD | Structured version Visualization version Unicode version |
Description: The following User's Proof is a Virtual Deduction proof (see wvd1 38785)
using conjunction-form virtual hypothesis collections. The
conjunction-form version of completeusersproof.cmd. It allows the User
to avoid superflous virtual hypotheses. This proof was completed
automatically by a tools program which invokes Mel L. O'Cat's
mmj2 and Norm Megill's Metamath Proof Assistant. suctrALTcf 39158
is suctrALTcfVD 39159 without virtual deductions and was derived
automatically from suctrALTcfVD 39159. The version of
completeusersproof.cmd used is capable of only generating
conjunction-form unification theorems, not unification deductions.
(Contributed by Alan Sare, 13-Jun-2015.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
Ref | Expression |
---|---|
suctrALTcfVD |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sssucid 5802 | . . . . . . . 8 | |
2 | idn1 38790 | . . . . . . . . 9 | |
3 | idn1 38790 | . . . . . . . . . 10 | |
4 | simpl 473 | . . . . . . . . . 10 | |
5 | 3, 4 | el1 38853 | . . . . . . . . 9 |
6 | idn1 38790 | . . . . . . . . 9 | |
7 | trel 4759 | . . . . . . . . . 10 | |
8 | 7 | 3impib 1262 | . . . . . . . . 9 |
9 | 2, 5, 6, 8 | el123 38991 | . . . . . . . 8 |
10 | ssel2 3598 | . . . . . . . 8 | |
11 | 1, 9, 10 | el0321old 38942 | . . . . . . 7 |
12 | 11 | int3 38837 | . . . . . 6 |
13 | idn1 38790 | . . . . . . . . 9 | |
14 | eleq2 2690 | . . . . . . . . . 10 | |
15 | 14 | biimpac 503 | . . . . . . . . 9 |
16 | 5, 13, 15 | el12 38953 | . . . . . . . 8 |
17 | 1, 16, 10 | el021old 38926 | . . . . . . 7 |
18 | 17 | int2 38831 | . . . . . 6 |
19 | simpr 477 | . . . . . . . 8 | |
20 | 3, 19 | el1 38853 | . . . . . . 7 |
21 | elsuci 5791 | . . . . . . 7 | |
22 | 20, 21 | el1 38853 | . . . . . 6 |
23 | jao 534 | . . . . . . 7 | |
24 | 23 | 3imp 1256 | . . . . . 6 |
25 | 12, 18, 22, 24 | el2122old 38944 | . . . . 5 |
26 | 25 | int2 38831 | . . . 4 |
27 | 26 | gen12 38843 | . . 3 |
28 | dftr2 4754 | . . . 4 | |
29 | 28 | biimpri 218 | . . 3 |
30 | 27, 29 | el1 38853 | . 2 |
31 | 30 | in1 38787 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wo 383 wa 384 wal 1481 wceq 1483 wcel 1990 wss 3574 wtr 4752 csuc 5725 |
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-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-un 3579 df-in 3581 df-ss 3588 df-sn 4178 df-uni 4437 df-tr 4753 df-suc 5729 df-vd1 38786 df-vhc2 38797 df-vhc3 38805 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |