Theorem pm2.61ne 1632

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 1586	. . 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 955   =/= wne 1584

This theorem is referenced by:  xrsupsslem 6037  xrinfmsslem 6038  infxpdom 7550  infmap2 7560  sm1cnilem 8333  nmlnoubi 8441  nmblolbii 8443  blocnilem 8448  blocni 8449  pjthlem13 9219  nmbdoplb 9940  cnlnadjlem7 9997  branmfnt 10029  pjbdln 10067  shatomistic 10279

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 1586

Copyright terms: Public domain