Theorem simpl 22

Description: Extract an assumption from the context.

Hypotheses

Ref	Expression
ax-simpl.1	|- R:*
ax-simpl.2	|- S:*

Assertion

Ref	Expression
simpl	|- (R, S) |= R

Proof of Theorem simpl

Step	Hyp	Ref	Expression
1		ax-simpl.1	. 2 |- R:*
2		ax-simpl.2	. 2 |- S:*
3	1, 2	ax-simpl 20	1 |- (R, S) |= R

Syntax hints:  *hb 3  kct 10   |= wffMMJ2 11  wffMMJ2t 12

This theorem was proved from axioms:  ax-simpl 20

This theorem is referenced by:  syldan  34  simpld  35  ancoms  49  adantr  50  ct2  53  an32s  55  anassrs  57  dfan2  144  notval2  149  notnot1  150  olc  154  orc  155  ax4e  158  exmid  186  ax2  191  ax8  198  ax11  201  axpow  208