Theorem prtlem90 16246

Description: Lemma for prter2 16285.

Assertion

Ref	Expression
prtlem90	|- (-. A e. B -> (C e. B -> C =/= A))

Proof of Theorem prtlem90

Step	Hyp	Ref	Expression
1		olc 290	. . . . . . 7 |- ((-. A e. B /\ C e. B) -> ((A e. B /\ -. C e. B) \/ (-. A e. B /\ C e. B)))
2		ancom 482	. . . . . . . 8 |- ((-. A e. B /\ C e. B) <-> (C e. B /\ -. A e. B))
3	2	orbi2i 275	. . . . . . 7 |- (((A e. B /\ -. C e. B) \/ (-. A e. B /\ C e. B)) <-> ((A e. B /\ -. C e. B) \/ (C e. B /\ -. A e. B)))
4	1, 3	sylib 215	. . . . . 6 |- ((-. A e. B /\ C e. B) -> ((A e. B /\ -. C e. B) \/ (C e. B /\ -. A e. B)))
5		xor 734	. . . . . 6 |- (-. (A e. B <-> C e. B) <-> ((A e. B /\ -. C e. B) \/ (C e. B /\ -. A e. B)))
6	4, 5	sylibr 217	. . . . 5 |- ((-. A e. B /\ C e. B) -> -. (A e. B <-> C e. B))
7		eleq1 1957	. . . . 5 |- (A = C -> (A e. B <-> C e. B))
8	6, 7	nsyl 131	. . . 4 |- ((-. A e. B /\ C e. B) -> -. A = C)
9	8	ex 402	. . 3 |- (-. A e. B -> (C e. B -> -. A = C))
10		df-ne 2019	. . 3 |- (A =/= C <-> -. A = C)
11	9, 10	syl6ibr 230	. 2 |- (-. A e. B -> (C e. B -> A =/= C))
12		necom 2094	. 2 |- (A =/= C <-> C =/= A)
13	11, 12	syl6ib 229	1 |- (-. A e. B -> (C e. B -> C =/= A))

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

This theorem is referenced by:  prter2 16285

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-cleq 1877  df-clel 1880  df-ne 2019

Copyright terms: Public domain