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  4380  ssdomg  6947  negiso  9125  infrenegsupex  9818  xrnegiso  11813  infxrnegsupex  11814  cos01bnd  12309  cos1bnd  12310  cos2bnd  12311  sin4lt0  12318  egt2lt3  12331  epos  12332  ene1  12336  eap1  12337  slotslfn  13098  strslfvd  13114  strslfv2d  13115  strsl0  13121  setsslid  13123  setsslnid  13124  sravscag  14447  reeff1o  15487  pigt2lt4  15498  pire  15500  pipos  15502  sinhalfpi  15510  tan4thpi  15555  sincos3rdpi  15557  pigt3  15558  lgsdir2lem4  15750  lgsdir2lem5  15751