Theorem simpli 109

Description: Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.)

Hypothesis

Ref	Expression
simpli.1	|- ( ph /\ ps )

Assertion

Ref	Expression
simpli	|- ph

Proof of Theorem simpli

Step	Hyp	Ref	Expression
1		simpli.1	. 2 |- ( ph /\ ps )
2		simpl 107	. 2 |- ( ( ph /\ ps ) -> ph )
3	1, 2	ax-mp 7	1 |- ph

Syntax hints:   /\ wa 102

This theorem was proved from axioms:  ax-mp 7  ax-ia1 104

This theorem is referenced by:  bi1  116  bi2  128  dfbi2  380  orc  668  pwundifss  4112  ssdomg  6493  negiso  8414  infrenegsupex  9080  cos01bnd  11045  cos1bnd  11046  cos2bnd  11047  sin4lt0  11053  egt2lt3  11063  epos  11064  ene1  11068  eap1  11069