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  4430  ssdomg  7065  negiso  9288  infrenegsupex  10004  xrnegiso  12047  infxrnegsupex  12048  cos01bnd  12544  cos1bnd  12545  cos2bnd  12546  sin4lt0  12553  egt2lt3  12566  epos  12567  ene1  12571  eap1  12572  slotslfn  13430  strslfvd  13446  strslfv2d  13447  strsl0  13453  setsslid  13455  setsslnid  13456  slotm  13467  sravscag  14864  reeff1o  15965  pigt2lt4  15977  pire  15979  pipos  15981  sinhalfpi  15989  tan4thpi  16034  sincos3rdpi  16036  pigt3  16037  logdivlt  16088  ppiublem1  16252  chtqub  16257  bposlem7  16278  lgsdir2lem4  16316  lgsdir2lem5  16317