Theorem pm2.61ine 2593

Description: Inference eliminating an inequality in an antecedent. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
pm2.61ine.1	⊢ (A = B → φ)
pm2.61ine.2	⊢ (A ≠ B → φ)

Assertion

Ref	Expression
pm2.61ine	⊢ φ

Proof of Theorem pm2.61ine

Step	Hyp	Ref	Expression
1		pm2.61ine.2	. 2 ⊢ (A ≠ B → φ)
2		nne 2521	. . 3 ⊢ (¬ A ≠ B ↔ A = B)
3		pm2.61ine.1	. . 3 ⊢ (A = B → φ)
4	2, 3	sylbi 187	. 2 ⊢ (¬ A ≠ B → φ)
5	1, 4	pm2.61i 156	1 ⊢ φ

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1642   ≠ wne 2517

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

This theorem depends on definitions:  df-bi 177  df-ne 2519

This theorem is referenced by:  rgenz  3656  raaan  3658  raaanv  3659  iinrab2  4030  riinrab  4042  nnsucelr  4429  lenltfin  4470  tfincl  4493  tfin11  4494  tfinltfinlem1  4501  tfinltfin  4502  vfinncvntnn  4549  dmxpid  4925  dmxpss  5053  rnxpid  5055  xpexr  5110  fconstfv  5457  mapsspm  6022  mapsspw  6023  enadj  6061  nc0le1  6217