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  6951  negiso  9134  infrenegsupex  9827  xrnegiso  11822  infxrnegsupex  11823  cos01bnd  12318  cos1bnd  12319  cos2bnd  12320  sin4lt0  12327  egt2lt3  12340  epos  12341  ene1  12345  eap1  12346  slotslfn  13107  strslfvd  13123  strslfv2d  13124  strsl0  13130  setsslid  13132  setsslnid  13133  sravscag  14456  reeff1o  15496  pigt2lt4  15507  pire  15509  pipos  15511  sinhalfpi  15519  tan4thpi  15564  sincos3rdpi  15566  pigt3  15567  lgsdir2lem4  15759  lgsdir2lem5  15760