Theorem simpli 110

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 108	. 2 |- ( ( ph /\ ps ) -> ph )
3	1, 2	ax-mp 5	1 |- ph

Syntax hints:   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-ia1 105

This theorem is referenced by:  biimp  117  biimpr  129  dfbi2  386  orc  702  pwundifss  4263  ssdomg  6744  negiso  8850  infrenegsupex  9532  xrnegiso  11203  infxrnegsupex  11204  cos01bnd  11699  cos1bnd  11700  cos2bnd  11701  sin4lt0  11707  egt2lt3  11720  epos  11721  ene1  11725  eap1  11726  slotslfn  12420  strslfvd  12435  strslfv2d  12436  strsl0  12442  setsslid  12444  setsslnid  12445  reeff1o  13334  pigt2lt4  13345  pire  13347  pipos  13349  sinhalfpi  13357  tan4thpi  13402  sincos3rdpi  13404  pigt3  13405  lgsdir2lem4  13572  lgsdir2lem5  13573