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  4388  ssdomg  6995  negiso  9177  infrenegsupex  9872  xrnegiso  11885  infxrnegsupex  11886  cos01bnd  12382  cos1bnd  12383  cos2bnd  12384  sin4lt0  12391  egt2lt3  12404  epos  12405  ene1  12409  eap1  12410  slotslfn  13171  strslfvd  13187  strslfv2d  13188  strsl0  13194  setsslid  13196  setsslnid  13197  sravscag  14522  reeff1o  15567  pigt2lt4  15578  pire  15580  pipos  15582  sinhalfpi  15590  tan4thpi  15635  sincos3rdpi  15637  pigt3  15638  lgsdir2lem4  15833  lgsdir2lem5  15834