Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > minimp-ax2c | Structured version Visualization version Unicode version | ||
| Description: Derivation of a commuted form of ax-2 7 from ax-mp 5 and minimp 1560. (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| minimp-ax2c |
     
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | minimp 1560 |
. . 3
| |
| 2 | minimp 1560 |
. . 3
| |
| 3 | 1, 2 | ax-mp 5 |
. 2
|
| 4 | minimp 1560 |
. . . 4
| |
| 5 | minimp 1560 |
. . . . . 6
| |
| 6 | minimp 1560 |
. . . . . . 7
| |
| 7 | minimp 1560 |
. . . . . . . 8
| |
| 8 | minimp 1560 |
. . . . . . . 8
| |
| 9 | minimp 1560 |
. . . . . . . 8
| |
| 10 | 7, 8, 9 | mp2 9 |
. . . . . . 7
|
| 11 | minimp 1560 |
. . . . . . . 8
| |
| 12 | 5, 11 | ax-mp 5 |
. . . . . . 7
|
| 13 | 6, 10, 12 | mp2 9 |
. . . . . 6
|
| 14 | minimp 1560 |
. . . . . 6
| |
| 15 | 5, 13, 14 | mp2 9 |
. . . . 5
|
| 16 | minimp-sylsimp 1561 |
. . . . 5
| |
| 17 | 15, 16 | ax-mp 5 |
. . . 4
|
| 18 | minimp 1560 |
. . . 4
| |
| 19 | 4, 17, 18 | mp2 9 |
. . 3
|
| 20 | minimp-sylsimp 1561 |
. . 3
| |
| 21 | 19, 20 | ax-mp 5 |
. 2
|
| 22 | minimp 1560 |
. . . 4
| |
| 23 | minimp 1560 |
. . . . 5
| |
| 24 | minimp 1560 |
. . . . 5
| |
| 25 | 23, 24 | ax-mp 5 |
. . . 4
|
| 26 | minimp 1560 |
. . . 4
| |
| 27 | 22, 25, 26 | mp2 9 |
. . 3
|
| 28 | minimp-sylsimp 1561 |
. . 3
| |
| 29 | minimp-sylsimp 1561 |
. . 3
| |
| 30 | 27, 28, 29 | mp2 9 |
. 2
|
| 31 | 3, 21, 30 | mp2 9 |
1
|
| Colors of variables: wff setvar class |
| Syntax hints: wi 4 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
| This theorem is referenced by: minimp-ax2 1564 |
| Copyright terms: Public domain | W3C validator |