Theorem pm2.61ne 1630

Description: Deduction eliminating an inequality in an antecedent.

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.1	. . . 4 |- (A = B -> (ps <-> ch))
2		pm2.61ne.3	. . . 4 |- (ph -> ch)
3	1, 2	syl5bir 210	. . 3 |- (A = B -> (ph -> ps))
4	3	impcom 351	. 2 |- ((ph /\ A = B) -> ps)
5		pm2.61ne.2	. . 3 |- ((ph /\ A =/= B) -> ps)
6		df-ne 1584	. . 3 |- (A =/= B <-> -. A = B)
7	5, 6	sylan2br 453	. 2 |- ((ph /\ -. A = B) -> ps)
8	4, 7	pm2.61dan 477	1 |- (ph -> ps)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223   = wceq 954   =/= wne 1582

This theorem is referenced by:  xrsupsslem 6031  xrinfmsslem 6032  infxpdom 7522  infmap2 7531  sm1cnilem 8294  nmlnoubi 8401  nmblolbii 8403  blocnilem 8408  blocni 8409  pjthlem13 9169  nmbdoplb 9887  cnlnadjlem7 9944  branmfnt 9976  pjbdln 10014  shatomistic 10225

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-an 225  df-ne 1584

Copyright terms: Public domain