Description: Obsolete version of mobii as of 24-Sep-2023. (Contributed by NM, 9-Mar-1995) (Revised by Mario Carneiro, 17-Oct-2016) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | mobii.1 | |- ( ps <-> ch ) |
|
Assertion | mobiiOLD | |- ( E* x ps <-> E* x ch ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mobii.1 | |- ( ps <-> ch ) |
|
2 | mobi | |- ( A. x ( ps <-> ch ) -> ( E* x ps <-> E* x ch ) ) |
|
3 | 2 1 | mpg | |- ( E* x ps <-> E* x ch ) |