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  4350  ssdomg  6893  negiso  9063  infrenegsupex  9750  xrnegiso  11688  infxrnegsupex  11689  cos01bnd  12184  cos1bnd  12185  cos2bnd  12186  sin4lt0  12193  egt2lt3  12206  epos  12207  ene1  12211  eap1  12212  slotslfn  12973  strslfvd  12989  strslfv2d  12990  strsl0  12996  setsslid  12998  setsslnid  12999  sravscag  14320  reeff1o  15360  pigt2lt4  15371  pire  15373  pipos  15375  sinhalfpi  15383  tan4thpi  15428  sincos3rdpi  15430  pigt3  15431  lgsdir2lem4  15623  lgsdir2lem5  15624