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  713  pwundifss  4320  ssdomg  6837  negiso  8982  infrenegsupex  9668  xrnegiso  11427  infxrnegsupex  11428  cos01bnd  11923  cos1bnd  11924  cos2bnd  11925  sin4lt0  11932  egt2lt3  11945  epos  11946  ene1  11950  eap1  11951  slotslfn  12704  strslfvd  12720  strslfv2d  12721  strsl0  12727  setsslid  12729  setsslnid  12730  sravscag  13999  reeff1o  15009  pigt2lt4  15020  pire  15022  pipos  15024  sinhalfpi  15032  tan4thpi  15077  sincos3rdpi  15079  pigt3  15080  lgsdir2lem4  15272  lgsdir2lem5  15273