Description: orbi1 with order of disjuncts reversed. Derived from orbi1rVD . (Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | orbi1r | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id | |
|
2 | 1 | orbi2d | |