Description: Alternate proof of dral1 , shorter but requiring ax-11 . (Contributed by NM, 24-Nov-1994) (Proof shortened by Wolf Lammen, 22-Apr-2018) (New usage is discouraged.) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | dral1.1 | |- ( A. x x = y -> ( ph <-> ps ) ) |
|
Assertion | dral1ALT | |- ( A. x x = y -> ( A. x ph <-> A. y ps ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dral1.1 | |- ( A. x x = y -> ( ph <-> ps ) ) |
|
2 | 1 | dral2 | |- ( A. x x = y -> ( A. x ph <-> A. x ps ) ) |
3 | axc11 | |- ( A. x x = y -> ( A. x ps -> A. y ps ) ) |
|
4 | axc11r | |- ( A. x x = y -> ( A. y ps -> A. x ps ) ) |
|
5 | 3 4 | impbid | |- ( A. x x = y -> ( A. x ps <-> A. y ps ) ) |
6 | 2 5 | bitrd | |- ( A. x x = y -> ( A. x ph <-> A. y ps ) ) |