Theorem simpr 23

Description: Extract an assumption from the context.

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  36  ancoms  49  ct1  52  sylan  54  an32s  55  anassrs  57  dfan2  144  imp  147  ex  148  notval2  149  notnot1  150  olc  154  orc  155  exlimdv2  156  exlimd  171  exmid  186  notnot  187  ax1  190  ax2  191  ax3  192  ax8  198  ax11  201  ax13  203  ax14  204