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  9287  infrenegsupex  10003  xrnegiso  12044  infxrnegsupex  12045  cos01bnd  12541  cos1bnd  12542  cos2bnd  12543  sin4lt0  12550  egt2lt3  12563  epos  12564  ene1  12568  eap1  12569  slotslfn  13427  strslfvd  13443  strslfv2d  13444  strsl0  13450  setsslid  13452  setsslnid  13453  slotm  13464  sravscag  14829  reeff1o  15923  pigt2lt4  15935  pire  15937  pipos  15939  sinhalfpi  15947  tan4thpi  15992  sincos3rdpi  15994  pigt3  15995  logdivlt  16046  ppiublem1  16192  lgsdir2lem4  16248  lgsdir2lem5  16249