Description: Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sylancr.1 | |
|
sylancr.2 | |
||
sylancr.3 | |
||
Assertion | sylancr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylancr.1 | |
|
2 | sylancr.2 | |
|
3 | sylancr.3 | |
|
4 | 1 | a1i | |
5 | 4 2 3 | syl2anc | |