Theorem simpli 111

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 109	. 2 |- ( ( ph /\ ps ) -> ph )
3	1, 2	ax-mp 5	1 |- ph

Syntax hints:   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-ia1 106

This theorem is referenced by:  biimp  118  biimpr  130  dfbi2  388  orc  714  pwundifss  4332  ssdomg  6870  negiso  9028  infrenegsupex  9715  xrnegiso  11573  infxrnegsupex  11574  cos01bnd  12069  cos1bnd  12070  cos2bnd  12071  sin4lt0  12078  egt2lt3  12091  epos  12092  ene1  12096  eap1  12097  slotslfn  12858  strslfvd  12874  strslfv2d  12875  strsl0  12881  setsslid  12883  setsslnid  12884  sravscag  14205  reeff1o  15245  pigt2lt4  15256  pire  15258  pipos  15260  sinhalfpi  15268  tan4thpi  15313  sincos3rdpi  15315  pigt3  15316  lgsdir2lem4  15508  lgsdir2lem5  15509