Theorem ralcom2 3022

Description: Commutation of restricted universal quantifiers. Note that and need not be distinct (this makes the proof longer). (Contributed by NM, 24-Nov-1994.) (Proof shortened by Mario Carneiro, 17-Oct-2016.)

Assertion

Ref	Expression
ralcom2

Distinct variable groups:   ,   ,

Proof of Theorem ralcom2

Step	Hyp	Ref	Expression
1		eleq1 2529	. . . . . . 7
2	1	sps 1865	. . . . . 6
3	2	imbi1d 317	. . . . . . . . 9
4	3	dral1 2067	. . . . . . . 8
5	4	bicomd 201	. . . . . . 7
6		df-ral 2812	. . . . . . 7
7		df-ral 2812	. . . . . . 7
8	5, 6, 7	3bitr4g 288	. . . . . 6
9	2, 8	imbi12d 320	. . . . 5
10	9	dral1 2067	. . . 4
11		df-ral 2812	. . . 4
12		df-ral 2812	. . . 4
13	10, 11, 12	3bitr4g 288	. . 3
14	13	biimpd 207	. 2
15		nfnae 2058	. . . . 5
16		nfra2 2844	. . . . 5
17	15, 16	nfan 1928	. . . 4
18		nfnae 2058	. . . . . . . 8
19		nfra1 2838	. . . . . . . 8
20	18, 19	nfan 1928	. . . . . . 7
21		nfcvf 2644	. . . . . . . . 9
22	21	adantr 465	. . . . . . . 8
23		nfcvd 2620	. . . . . . . 8
24	22, 23	nfeld 2627	. . . . . . 7
25	20, 24	nfan1 1927	. . . . . 6
26		rsp2 2831	. . . . . . . . 9
27	26	ancomsd 454	. . . . . . . 8
28	27	expdimp 437	. . . . . . 7
29	28	adantll 713	. . . . . 6
30	25, 29	ralrimi 2857	. . . . 5
31	30	ex 434	. . . 4
32	17, 31	ralrimi 2857	. . 3
33	32	ex 434	. 2
34	14, 33	pm2.61i 164	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  e.wcel 1818  F/_wnfc 2605  A.wral 2807

This theorem is referenced by:  tz7.48lem  7125  tratrb  33307  tratrbVD  33661  imo72b2  37993

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-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812