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  719  pwundifss  4382  ssdomg  6952  negiso  9135  infrenegsupex  9828  xrnegiso  11840  infxrnegsupex  11841  cos01bnd  12337  cos1bnd  12338  cos2bnd  12339  sin4lt0  12346  egt2lt3  12359  epos  12360  ene1  12364  eap1  12365  slotslfn  13126  strslfvd  13142  strslfv2d  13143  strsl0  13149  setsslid  13151  setsslnid  13152  sravscag  14476  reeff1o  15516  pigt2lt4  15527  pire  15529  pipos  15531  sinhalfpi  15539  tan4thpi  15584  sincos3rdpi  15586  pigt3  15587  lgsdir2lem4  15779  lgsdir2lem5  15780