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  392  orc  724  pwundifss  4425  ssdomg  7055  negiso  9275  infrenegsupex  9973  xrnegiso  12006  infxrnegsupex  12007  cos01bnd  12503  cos1bnd  12504  cos2bnd  12505  sin4lt0  12512  egt2lt3  12525  epos  12526  ene1  12530  eap1  12531  slotslfn  13356  strslfvd  13372  strslfv2d  13373  strsl0  13379  setsslid  13381  setsslnid  13382  sravscag  14752  reeff1o  15797  pigt2lt4  15808  pire  15810  pipos  15812  sinhalfpi  15820  tan4thpi  15865  sincos3rdpi  15867  pigt3  15868  lgsdir2lem4  16064  lgsdir2lem5  16065