Description: An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mp3an2ani.1 | |
|
mp3an2ani.2 | |
||
mp3an2ani.3 | |
||
mp3an2ani.4 | |
||
Assertion | mp3an2ani | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an2ani.1 | |
|
2 | mp3an2ani.2 | |
|
3 | mp3an2ani.3 | |
|
4 | mp3an2ani.4 | |
|
5 | 1 2 3 4 | mp3an3an | |
6 | 5 | anabss5 | |