Description: Virtual deduction identity rule which is idd with virtual deduction symbols. (Contributed by Alan Sare, 21-Apr-2011) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | idn2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idd | |
|
2 | 1 | dfvd2ir | |