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  4432  ssdomg  7071  negiso  9293  infrenegsupex  10009  xrnegiso  12052  infxrnegsupex  12053  cos01bnd  12549  cos1bnd  12550  cos2bnd  12551  sin4lt0  12558  egt2lt3  12571  epos  12572  ene1  12576  eap1  12577  slotslfn  13435  strslfvd  13451  strslfv2d  13452  strsl0  13458  setsslid  13460  setsslnid  13461  slotm  13472  sravscag  14888  reeff1o  16016  pigt2lt4  16028  pire  16030  pipos  16032  sinhalfpi  16040  tan4thpi  16085  sincos3rdpi  16087  pigt3  16088  logdivlt  16141  ppiublem1  16308  chtqub  16313  bposlem7  16334  lgsdir2lem4  16372  lgsdir2lem5  16373