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

Syntax hints:   /\ wa 104

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

This theorem is referenced by:  biimp  118  biimpr  130  dfbi2  388  orc  712  pwundifss  4283  ssdomg  6773  negiso  8906  infrenegsupex  9588  xrnegiso  11261  infxrnegsupex  11262  cos01bnd  11757  cos1bnd  11758  cos2bnd  11759  sin4lt0  11765  egt2lt3  11778  epos  11779  ene1  11783  eap1  11784  slotslfn  12478  strslfvd  12494  strslfv2d  12495  strsl0  12501  setsslid  12503  setsslnid  12504  reeff1o  13976  pigt2lt4  13987  pire  13989  pipos  13991  sinhalfpi  13999  tan4thpi  14044  sincos3rdpi  14046  pigt3  14047  lgsdir2lem4  14214  lgsdir2lem5  14215