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  4375  ssdomg  6928  negiso  9098  infrenegsupex  9785  xrnegiso  11768  infxrnegsupex  11769  cos01bnd  12264  cos1bnd  12265  cos2bnd  12266  sin4lt0  12273  egt2lt3  12286  epos  12287  ene1  12291  eap1  12292  slotslfn  13053  strslfvd  13069  strslfv2d  13070  strsl0  13076  setsslid  13078  setsslnid  13079  sravscag  14401  reeff1o  15441  pigt2lt4  15452  pire  15454  pipos  15456  sinhalfpi  15464  tan4thpi  15509  sincos3rdpi  15511  pigt3  15512  lgsdir2lem4  15704  lgsdir2lem5  15705