Theorem simpr 23

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
simpr	⊢ (R, S)⊧S

Proof of Theorem simpr

Step	Hyp	Ref	Expression
1		ax-simpl.1	. 2 ⊢ R:∗
2		ax-simpl.2	. 2 ⊢ S:∗
3	1, 2	ax-simpr 21	1 ⊢ (R, S)⊧S

Syntax hints:  ∗hb 3  kct 10  ⊧wffMMJ2 11  wffMMJ2t 12

This theorem was proved from axioms:  ax-simpr 21

This theorem is referenced by:  simprd  38  ancoms  54  ct1  57  sylan  59  an32s  60  anassrs  62  dfan2  154  imp  157  ex  158  notval2  159  notnot1  160  olc  164  orc  165  exlimdv2  166  exlimd  183  exmid  199  notnot  200  ax1  203  ax2  204  ax3  205  ax8  211  ax11  214  ax13  216  ax14  217