Theorem prel12 4207

Description: Equality of two unordered pairs. (Contributed by NM, 17-Oct-1996.)

Hypotheses

Ref	Expression
preq12b.1
preq12b.2
preq12b.3
preq12b.4

Assertion

Ref	Expression
prel12

Proof of Theorem prel12

Step	Hyp	Ref	Expression
1		preq12b.1	. . . . 5
2	1	prid1 4138	. . . 4
3		eleq2 2530	. . . 4
4	2, 3	mpbii 211	. . 3
5		preq12b.2	. . . . 5
6	5	prid2 4139	. . . 4
7		eleq2 2530	. . . 4
8	6, 7	mpbii 211	. . 3
9	4, 8	jca 532	. 2
10	1	elpr 4047	. . . 4
11		eqeq2 2472	. . . . . . . . . . . 12
12	11	notbid 294	. . . . . . . . . . 11
13		orel2 383	. . . . . . . . . . 11
14	12, 13	syl6bi 228	. . . . . . . . . 10
15	14	com3l 81	. . . . . . . . 9
16	15	imp 429	. . . . . . . 8
17	16	ancrd 554	. . . . . . 7
18		eqeq2 2472	. . . . . . . . . . . 12
19	18	notbid 294	. . . . . . . . . . 11
20		orel1 382	. . . . . . . . . . 11
21	19, 20	syl6bi 228	. . . . . . . . . 10
22	21	com3l 81	. . . . . . . . 9
23	22	imp 429	. . . . . . . 8
24	23	ancrd 554	. . . . . . 7
25	17, 24	orim12d 838	. . . . . 6
26	5	elpr 4047	. . . . . . 7
27		orcom 387	. . . . . . 7
28	26, 27	bitri 249	. . . . . 6
29		preq12b.3	. . . . . . 7
30		preq12b.4	. . . . . . 7
31	1, 5, 29, 30	preq12b 4206	. . . . . 6
32	25, 28, 31	3imtr4g 270	. . . . 5
33	32	ex 434	. . . 4
34	10, 33	syl5bi 217	. . 3
35	34	impd 431	. 2
36	9, 35	impbid2 204	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368  /\wa 369  =wceq 1395  e.wcel 1818  cvv 3109  {cpr 4031

This theorem is referenced by:  prel12g  4210  dfac2  8532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-sn 4030  df-pr 4032