Theorem simpl 22

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
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  36  simpld  37  ancoms  54  adantr  55  ct2  58  an32s  60  anassrs  62  dfan2  154  notval2  159  notnot1  160  olc  164  orc  165  ax4e  168  exmid  199  ax2  204  ax8  211  ax11  214  axpow  221