Theorem pm2.61ine 1610

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 1563	. . 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 1099   =/= wne 1561

This theorem is referenced by:  raaan 2331  onfr 2949  dmxpid 3292  dmxpss 3422  rnxpss 3423  xpexr 3425  cnvpo 3463  fconst 3597  fconstfv 3788  fodomr 4417  inf3lemd 4536  msqge0 5539  abs1m 6792  bcpasc 6858  mulc1cncf 7165  siii 8379  cnfilca 8801  occllem7 9309  riesz3 10124  unierr 10164

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 1563

Copyright terms: Public domain