Description: An inference based on modus ponens. (Contributed by NM, 14-May-1999)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mp3an.1 | |
|
mp3an.2 | |
||
mp3an.3 | |
||
mp3an.4 | |
||
Assertion | mp3an | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an.1 | |
|
2 | mp3an.2 | |
|
3 | mp3an.3 | |
|
4 | mp3an.4 | |
|
5 | 1 4 | mp3an1 | |
6 | 2 3 5 | mp2an | |