Theorem simpli 110

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 108	. 2 |- ( ( ph /\ ps ) -> ph )
3	1, 2	ax-mp 5	1 |- ph

Syntax hints:   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-ia1 105

This theorem is referenced by:  biimp  117  biimpr  129  dfbi2  386  orc  702  pwundifss  4240  ssdomg  6712  negiso  8805  infrenegsupex  9484  xrnegiso  11136  infxrnegsupex  11137  cos01bnd  11632  cos1bnd  11633  cos2bnd  11634  sin4lt0  11640  egt2lt3  11653  epos  11654  ene1  11658  eap1  11659  slotslfn  12155  strslfvd  12170  strslfv2d  12171  strsl0  12177  setsslid  12179  setsslnid  12180  reeff1o  13033  pigt2lt4  13044  pire  13046  pipos  13048  sinhalfpi  13056  tan4thpi  13101  sincos3rdpi  13103  pigt3  13104