Metamath Proof Explorer
Description: Inference from existential specialization. (Contributed by NM, 19-Aug-1993) (Revised by Wolf Lammen, 22-Oct-2023)
|
|
Ref |
Expression |
|
Hypotheses |
speiv.1 |
|
|
|
speiv.2 |
|
|
Assertion |
speiv |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
speiv.1 |
|
2 |
|
speiv.2 |
|
3 |
2
|
hbth |
|
4 |
3 1
|
spimew |
|
5 |
2 4
|
ax-mp |
|