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

This proof depends on syntax axioms:   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-ia1 106

This theorem is used by:  biimp  118  biimpr  130  dfbi2  392  orc  724  pwundifss  4430  ssdomg  7065  negiso  9285  infrenegsupex  9994  xrnegiso  12028  infxrnegsupex  12029  cos01bnd  12525  cos1bnd  12526  cos2bnd  12527  sin4lt0  12534  egt2lt3  12547  epos  12548  ene1  12552  eap1  12553  slotslfn  13378  strslfvd  13394  strslfv2d  13395  strsl0  13401  setsslid  13403  setsslnid  13404  slotm  13415  sravscag  14780  reeff1o  15874  pigt2lt4  15885  pire  15887  pipos  15889  sinhalfpi  15897  tan4thpi  15942  sincos3rdpi  15944  pigt3  15945  lgsdir2lem4  16150  lgsdir2lem5  16151