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  713  pwundifss  4321  ssdomg  6839  negiso  8985  infrenegsupex  9671  xrnegiso  11430  infxrnegsupex  11431  cos01bnd  11926  cos1bnd  11927  cos2bnd  11928  sin4lt0  11935  egt2lt3  11948  epos  11949  ene1  11953  eap1  11954  slotslfn  12715  strslfvd  12731  strslfv2d  12732  strsl0  12738  setsslid  12740  setsslnid  12741  sravscag  14025  reeff1o  15035  pigt2lt4  15046  pire  15048  pipos  15050  sinhalfpi  15058  tan4thpi  15103  sincos3rdpi  15105  pigt3  15106  lgsdir2lem4  15298  lgsdir2lem5  15299