Theorem pm2.61ine 1631

Description: Inference eliminating an inequality in an antecedent.

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.1	. 2 ⊢ (A = B → φ)
2		df-ne 1584	. . 3 ⊢ (A ≠ B ↔ ¬ A = B)
3		pm2.61ine.2	. . 3 ⊢ (A ≠ B → φ)
4	2, 3	sylbir 201	. 2 ⊢ (¬ A = B → φ)
5	1, 4	pm2.61i 126	1 ⊢ φ

Syntax hints:  ¬ wn 2   → wi 3   = wceq 954   ≠ wne 1582

This theorem is referenced by:  raaan 2356  onfr 2981  dmxpid 3328  dmxpss 3465  rnxpss 3466  xpexr 3471  cnvpo 3514  fconst 3649  fconstfv 3840  fodomr 4469  inf3lemd 4592  msqge0 5596  abs1m 6849  bcpasc 6915  mulc1cncf 7222  siii 8457  occllem7 9118  riesz3 9933  unierr 9975  cnfilca 10487

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 1584

Copyright terms: Public domain