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  717  pwundifss  4376  ssdomg  6938  negiso  9113  infrenegsupex  9801  xrnegiso  11788  infxrnegsupex  11789  cos01bnd  12284  cos1bnd  12285  cos2bnd  12286  sin4lt0  12293  egt2lt3  12306  epos  12307  ene1  12311  eap1  12312  slotslfn  13073  strslfvd  13089  strslfv2d  13090  strsl0  13096  setsslid  13098  setsslnid  13099  sravscag  14422  reeff1o  15462  pigt2lt4  15473  pire  15475  pipos  15477  sinhalfpi  15485  tan4thpi  15530  sincos3rdpi  15532  pigt3  15533  lgsdir2lem4  15725  lgsdir2lem5  15726