Higher-Order Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HOLE Home > Th. List > ax-syl | GIF version |
Description: Syllogism inference. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Ref | Expression |
---|---|
ax-syl.1 | ⊢ R⊧S |
ax-syl.2 | ⊢ S⊧T |
Ref | Expression |
---|---|
ax-syl | ⊢ R⊧T |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tr | . 2 term R | |
2 | tt | . 2 term T | |
3 | 1, 2 | wffMMJ2 11 | 1 wff R⊧T |
Colors of variables: type var term |
This axiom is referenced by: syl 16 |
Copyright terms: Public domain | W3C validator |