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  720  pwundifss  4406  ssdomg  7018  negiso  9229  infrenegsupex  9926  xrnegiso  11947  infxrnegsupex  11948  cos01bnd  12444  cos1bnd  12445  cos2bnd  12446  sin4lt0  12453  egt2lt3  12466  epos  12467  ene1  12471  eap1  12472  slotslfn  13238  strslfvd  13254  strslfv2d  13255  strsl0  13261  setsslid  13263  setsslnid  13264  sravscag  14591  reeff1o  15638  pigt2lt4  15649  pire  15651  pipos  15653  sinhalfpi  15661  tan4thpi  15706  sincos3rdpi  15708  pigt3  15709  lgsdir2lem4  15904  lgsdir2lem5  15905