Description: Virtual deduction proof of snelpwi . (Contributed by Alan Sare, 25-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | snelpwrVD | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | snex | |
|
2 | idn1 | |
|
3 | snssi | |
|
4 | 2 3 | e1a | |
5 | elpwg | |
|
6 | 5 | biimprd | |
7 | 1 4 6 | e01 | |
8 | 7 | in1 | |