ax-simpl - Higher-Order Logic Explorer

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

Axiom ax-simpl 20

Description: Extract an assumption from the context.

**Hypotheses**
Ref	Expression
ax-simpl.1	⊢ R:∗
ax-simpl.2	⊢ S:∗

**Assertion**
Ref	Expression
ax-simpl	⊢ (R, S)⊧R

**Detailed syntax breakdown of Axiom ax-simpl**
Step	Hyp	Ref	Expression
1		tr	. . 3 term R
2		ts	. . 3 term S
3	1, 2	kct 10	. 2 term (R, S)
4	3, 1	wffMMJ2 11	1 wff (R, S)⊧R

Colors of variables: type var term

This axiom is referenced by: simpl 22