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  712  pwundifss  4287  ssdomg  6781  negiso  8915  infrenegsupex  9597  xrnegiso  11273  infxrnegsupex  11274  cos01bnd  11769  cos1bnd  11770  cos2bnd  11771  sin4lt0  11777  egt2lt3  11790  epos  11791  ene1  11795  eap1  11796  slotslfn  12491  strslfvd  12507  strslfv2d  12508  strsl0  12514  setsslid  12516  setsslnid  12517  sravscag  13568  reeff1o  14382  pigt2lt4  14393  pire  14395  pipos  14397  sinhalfpi  14405  tan4thpi  14450  sincos3rdpi  14452  pigt3  14453  lgsdir2lem4  14620  lgsdir2lem5  14621