Theorem pm2.61ne 2087

Description: Deduction eliminating an inequality in an antecedent. (The proof was shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
pm2.61ne.1	|- (A = B -> (ps <-> ch))
pm2.61ne.2	|- ((ph /\ A =/= B) -> ps)
pm2.61ne.3	|- (ph -> ch)

Assertion

Ref	Expression
pm2.61ne	|- (ph -> ps)

Proof of Theorem pm2.61ne

Step	Hyp	Ref	Expression
1		pm2.61ne.2	. . 3 |- ((ph /\ A =/= B) -> ps)
2	1	expcom 403	. 2 |- (A =/= B -> (ph -> ps))
3		nne 2021	. . 3 |- (-. A =/= B <-> A = B)
4		pm2.61ne.1	. . . 4 |- (A = B -> (ps <-> ch))
5		pm2.61ne.3	. . . 4 |- (ph -> ch)
6	4, 5	syl5bir 227	. . 3 |- (A = B -> (ph -> ps))
7	3, 6	sylbi 216	. 2 |- (-. A =/= B -> (ph -> ps))
8	2, 7	pm2.61i 140	1 |- (ph -> ps)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   =/= wne 2017

This theorem is referenced by:  xrsupsslem 7285  xrinfmsslem 7286  infxpdom 8840  infmap2 8850  sm1cnilem 9686  nmlnoubi 9796  nmblolbii 9799  blocnilem 9804  blocni 9805  pjthlem13 10864  nmbdoplbi 11586  cnlnadjlem7 11643  branmfn 11675  branmfnOLD 11676  pjbdlni 11720  shatomistici 11933  zornn0 15764  ps-1 17078

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 164  df-an 242  df-ne 2019

Copyright terms: Public domain