Axiom ax-simpr 21

Description: Extract an assumption from the context. (Contributed by Mario Carneiro, 8-Oct-2014.)

Hypotheses

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

Assertion

Ref	Expression
ax-simpr	⊢ (R, S)⊧S

Detailed syntax breakdown of Axiom ax-simpr

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, 2	wffMMJ2 11	1 wff (R, S)⊧S

This axiom is referenced by:  simpr  23