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  4321  ssdomg  6846  negiso  8999  infrenegsupex  9685  xrnegiso  11444  infxrnegsupex  11445  cos01bnd  11940  cos1bnd  11941  cos2bnd  11942  sin4lt0  11949  egt2lt3  11962  epos  11963  ene1  11967  eap1  11968  slotslfn  12729  strslfvd  12745  strslfv2d  12746  strsl0  12752  setsslid  12754  setsslnid  12755  sravscag  14075  reeff1o  15093  pigt2lt4  15104  pire  15106  pipos  15108  sinhalfpi  15116  tan4thpi  15161  sincos3rdpi  15163  pigt3  15164  lgsdir2lem4  15356  lgsdir2lem5  15357