Description: Syllogism inference with commutation of antecedents. (Contributed by NM, 2-Jul-2008)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sylancom.1 | |
|
sylancom.2 | |
||
Assertion | sylancom | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylancom.1 | |
|
2 | sylancom.2 | |
|
3 | simpr | |
|
4 | 1 3 2 | syl2anc | |