ax-syl - Higher-Order Logic Explorer

	Higher-Order Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > HOLE Home > Th. List > ax-syl		GIF version

Axiom ax-syl 15

Description: Syllogism inference. (Contributed by Mario Carneiro, 8-Oct-2014.)

**Hypotheses**
Ref	Expression
ax-syl.1	⊢ R⊧S
ax-syl.2	⊢ S⊧T

**Assertion**
Ref	Expression
ax-syl	⊢ R⊧T

**Detailed syntax breakdown of Axiom ax-syl**
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