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  7069  negiso  9293  infrenegsupex  10010  xrnegiso  12053  infxrnegsupex  12054  cos01bnd  12550  cos1bnd  12551  cos2bnd  12552  sin4lt0  12559  egt2lt3  12572  epos  12573  ene1  12577  eap1  12578  slotslfn  13436  strslfvd  13452  strslfv2d  13453  strsl0  13459  setsslid  13461  setsslnid  13462  slotm  13473  sravscag  14889  reeff1o  15999  pigt2lt4  16011  pire  16013  pipos  16015  sinhalfpi  16023  tan4thpi  16068  sincos3rdpi  16070  pigt3  16071  logdivlt  16124  ppiublem1  16291  chtqub  16296  bposlem7  16317  lgsdir2lem4  16355  lgsdir2lem5  16356