Theorem pm2.61ine 1634

Description: Inference eliminating an inequality in an antecedent.

Hypotheses

Ref	Expression
pm2.61ine.1	|- (A = B -> ph)
pm2.61ine.2	|- (A =/= B -> ph)

Assertion

Ref	Expression
pm2.61ine	|- ph

Proof of Theorem pm2.61ine

Step	Hyp	Ref	Expression
1		pm2.61ine.1	. 2 |- (A = B -> ph)
2		df-ne 1587	. . 3 |- (A =/= B <-> -. A = B)
3		pm2.61ine.2	. . 3 |- (A =/= B -> ph)
4	2, 3	sylbir 201	. 2 |- (-. A = B -> ph)
5	1, 4	pm2.61i 126	1 |- ph

Syntax hints:  -. wn 2   -> wi 3   = wceq 956   =/= wne 1585

This theorem is referenced by:  raaan 2360  onfr 2986  dmxpid 3333  dmxpss 3473  rnxpss 3474  xpexr 3479  cnvpo 3522  fconst 3658  fconstfv 3849  fodomr 4483  inf3lemd 4612  msqge0 5614  abs1m 6904  bcpasc 6969  mulc1cncf 7279  siii 8513  occllem7 9179  h1de2ctlem 9478  riesz3 9995  unierr 10037  cnfilca 10583  cnfilcaOLD 10584

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-ne 1587

Copyright terms: Public domain