Step | Hyp | Ref
| Expression |
1 | | breldm 4912 |
. . . . . . . . . 10
![(](lp.gif) ![x](_x.gif) ![F](_cf.gif) ![F](_cf.gif) ![)](rp.gif) |
2 | 1 | adantl 452 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![F](_cf.gif) ![y](_y.gif) ![F](_cf.gif) ![)](rp.gif) |
3 | | fnfrec.1 |
. . . . . . . . . . 11
FRec ![(](lp.gif) ![G](_cg.gif) ![I](_ci.gif) ![)](rp.gif) |
4 | | fnfrec.2 |
. . . . . . . . . . 11
![(](lp.gif) Funs ![)](rp.gif) |
5 | | fnfrec.3 |
. . . . . . . . . . 11
![(](lp.gif) ![G](_cg.gif) ![)](rp.gif) |
6 | | fnfrec.4 |
. . . . . . . . . . 11
![(](lp.gif) ![G](_cg.gif) ![)](rp.gif) |
7 | 3, 4, 5, 6 | dmfrec 6317 |
. . . . . . . . . 10
![(](lp.gif) Nn ![)](rp.gif) |
8 | 7 | adantr 451 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![F](_cf.gif) ![y](_y.gif) Nn ![)](rp.gif) |
9 | 2, 8 | eleqtrd 2429 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![F](_cf.gif) ![y](_y.gif) Nn ![)](rp.gif) |
10 | 9 | adantrr 697 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![F](_cf.gif) ![x](_x.gif) ![F](_cf.gif) ![z](_z.gif) ![)](rp.gif)
Nn ![)](rp.gif) |
11 | 3 | frecexg 6313 |
. . . . . . . . . . . 12
![(](lp.gif) Funs
![_V](rmcv.gif) ![)](rp.gif) |
12 | | fnfreclem1 6318 |
. . . . . . . . . . . 12
![(](lp.gif) ![{](lbrace.gif)
![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) ![_V](rmcv.gif) ![)](rp.gif) |
13 | 4, 11, 12 | 3syl 18 |
. . . . . . . . . . 11
![(](lp.gif) ![{](lbrace.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif)
![z](_z.gif) ![)](rp.gif)
![_V](rmcv.gif) ![)](rp.gif) |
14 | | breq1 4643 |
. . . . . . . . . . . . . 14
![(](lp.gif) 0c ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) 0c![F](_cf.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
15 | | breq1 4643 |
. . . . . . . . . . . . . 14
![(](lp.gif) 0c ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) 0c![F](_cf.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
16 | 14, 15 | anbi12d 691 |
. . . . . . . . . . . . 13
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) 0c![F](_cf.gif) 0c![F](_cf.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
17 | 16 | imbi1d 308 |
. . . . . . . . . . . 12
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![(](lp.gif) 0c![F](_cf.gif)
0c![F](_cf.gif) ![z](_z.gif)
![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
18 | 17 | 2albidv 1627 |
. . . . . . . . . . 11
![(](lp.gif) 0c ![(](lp.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) 0c![F](_cf.gif) 0c![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
19 | | breq1 4643 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
20 | | breq1 4643 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
21 | 19, 20 | anbi12d 691 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 21 | imbi1d 308 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
23 | 22 | 2albidv 1627 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
24 | | breq1 4643 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
25 | | breq1 4643 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
26 | 24, 25 | anbi12d 691 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
27 | 26 | imbi1d 308 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
28 | 27 | 2albidv 1627 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
29 | | breq2 4644 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![(](lp.gif) 1c![)](rp.gif) ![F](_cf.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
30 | | breq2 4644 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![(](lp.gif) 1c![)](rp.gif) ![F](_cf.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) |
31 | 29, 30 | bi2anan9 843 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif)
![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c![)](rp.gif) ![F](_cf.gif) ![(](lp.gif) 1c![)](rp.gif) ![F](_cf.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) 1c![)](rp.gif) ![F](_cf.gif)
![(](lp.gif) 1c![)](rp.gif) ![F](_cf.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
32 | | eqeq12 2365 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif)
![b](_b.gif) ![(](lp.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) |
33 | 31, 32 | imbi12d 311 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif)
![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c![)](rp.gif) ![F](_cf.gif) ![(](lp.gif) 1c![)](rp.gif) ![F](_cf.gif) ![b](_b.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
34 | 33 | cbval2v 2006 |
. . . . . . . . . . . 12
![(](lp.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![A.](forall.gif) ![a](_a.gif) ![A.](forall.gif) ![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c![)](rp.gif) ![F](_cf.gif)
![(](lp.gif) 1c![)](rp.gif) ![F](_cf.gif) ![b](_b.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) |
35 | 28, 34 | syl6bb 252 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![A.](forall.gif) ![a](_a.gif) ![A.](forall.gif) ![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![b](_b.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
36 | | breq1 4643 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![x](_x.gif) ![F](_cf.gif) ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
37 | | breq1 4643 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![x](_x.gif) ![F](_cf.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
38 | 36, 37 | anbi12d 691 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![(](lp.gif) ![x](_x.gif) ![F](_cf.gif) ![x](_x.gif) ![F](_cf.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
39 | 38 | imbi1d 308 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![F](_cf.gif) ![x](_x.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
40 | 39 | 2albidv 1627 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![w](_w.gif) ![F](_cf.gif) ![w](_w.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![F](_cf.gif) ![x](_x.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
41 | 3, 4, 5, 6 | fnfreclem2 6319 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) 0c![F](_cf.gif) ![I](_ci.gif) ![)](rp.gif) ![)](rp.gif) |
42 | 41 | imp 418 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) 0c![F](_cf.gif) ![y](_y.gif)
![I](_ci.gif) ![)](rp.gif) |
43 | 42 | adantrr 697 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) 0c![F](_cf.gif)
0c![F](_cf.gif) ![z](_z.gif) ![)](rp.gif) ![I](_ci.gif) ![)](rp.gif) |
44 | 3, 4, 5, 6 | fnfreclem2 6319 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) 0c![F](_cf.gif) ![I](_ci.gif) ![)](rp.gif) ![)](rp.gif) |
45 | 44 | imp 418 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) 0c![F](_cf.gif) ![z](_z.gif)
![I](_ci.gif) ![)](rp.gif) |
46 | 45 | adantrl 696 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) 0c![F](_cf.gif)
0c![F](_cf.gif) ![z](_z.gif) ![)](rp.gif) ![I](_ci.gif) ![)](rp.gif) |
47 | 43, 46 | eqtr4d 2388 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) 0c![F](_cf.gif)
0c![F](_cf.gif) ![z](_z.gif) ![)](rp.gif) ![z](_z.gif) ![)](rp.gif) |
48 | 47 | ex 423 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) 0c![F](_cf.gif)
0c![F](_cf.gif) ![z](_z.gif)
![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
49 | 48 | alrimivv 1632 |
. . . . . . . . . . 11
![(](lp.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) 0c![F](_cf.gif)
0c![F](_cf.gif) ![z](_z.gif)
![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
50 | 4 | ad2antrr 706 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![a](_a.gif) Funs ![)](rp.gif) |
51 | 5 | ad2antrr 706 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![a](_a.gif) ![G](_cg.gif) ![)](rp.gif) |
52 | 6 | ad2antrr 706 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![a](_a.gif) ![G](_cg.gif) ![)](rp.gif) |
53 | | simplr 731 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![a](_a.gif) Nn ![)](rp.gif) |
54 | | simpr 447 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![a](_a.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![a](_a.gif) ![)](rp.gif) |
55 | 3, 50, 51, 52, 53, 54 | fnfreclem3 6320 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![a](_a.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![y](_y.gif) ![G](_cg.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
56 | 55 | adantlrr 701 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
Nn ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![F](_cf.gif) ![a](_a.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![y](_y.gif) ![G](_cg.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
57 | 56 | ex 423 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif)
![z](_z.gif) ![)](rp.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![y](_y.gif) ![G](_cg.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
58 | 4 | ad2antrr 706 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![b](_b.gif) Funs ![)](rp.gif) |
59 | 5 | ad2antrr 706 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![b](_b.gif) ![G](_cg.gif) ![)](rp.gif) |
60 | 6 | ad2antrr 706 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![b](_b.gif) ![G](_cg.gif) ![)](rp.gif) |
61 | | simplr 731 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![b](_b.gif) Nn ![)](rp.gif) |
62 | | simpr 447 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![b](_b.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![b](_b.gif) ![)](rp.gif) |
63 | 3, 58, 59, 60, 61, 62 | fnfreclem3 6320 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![b](_b.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) |
64 | 63 | adantlrr 701 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
Nn ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![F](_cf.gif) ![b](_b.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) |
65 | 64 | ex 423 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif)
![z](_z.gif) ![)](rp.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
66 | 57, 65 | anim12d 546 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif)
![z](_z.gif) ![)](rp.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![b](_b.gif) ![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![y](_y.gif) ![G](_cg.gif) ![a](_a.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
67 | | eeanv 1913 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![y](_y.gif) ![G](_cg.gif) ![a](_a.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![y](_y.gif) ![G](_cg.gif) ![a](_a.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
68 | 66, 67 | syl6ibr 218 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif)
![z](_z.gif) ![)](rp.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![b](_b.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![y](_y.gif) ![G](_cg.gif) ![a](_a.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
69 | | 19.29 1596 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![y](_y.gif) ![G](_cg.gif) ![a](_a.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![y](_y.gif) ![G](_cg.gif) ![a](_a.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
70 | | 19.29 1596 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![y](_y.gif) ![G](_cg.gif) ![a](_a.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![y](_y.gif) ![G](_cg.gif) ![a](_a.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
71 | 70 | eximi 1576 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![y](_y.gif) ![G](_cg.gif) ![a](_a.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif)
![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![y](_y.gif) ![G](_cg.gif) ![a](_a.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
72 | 69, 71 | syl 15 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![y](_y.gif) ![G](_cg.gif) ![a](_a.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![y](_y.gif) ![G](_cg.gif) ![a](_a.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
73 | | pm3.35 570 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif)
![z](_z.gif) ![)](rp.gif) |
74 | | breq1 4643 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![G](_cg.gif) ![z](_z.gif) ![G](_cg.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
75 | 74 | anbi1d 685 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![G](_cg.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![(](lp.gif) ![z](_z.gif) ![G](_cg.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
76 | 75 | biimpa 470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![G](_cg.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif) ![(](lp.gif) ![z](_z.gif) ![G](_cg.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) |
77 | | elfunsi 5832 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
![(](lp.gif) Funs ![G](_cg.gif) ![)](rp.gif) |
78 | | funbrfv 5357 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
![(](lp.gif) ![(](lp.gif) ![z](_z.gif) ![G](_cg.gif) ![(](lp.gif) ![G](_cg.gif) ![`](backtick.gif) ![z](_z.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
79 | 4, 77, 78 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
![(](lp.gif) ![(](lp.gif) ![z](_z.gif) ![G](_cg.gif) ![(](lp.gif) ![G](_cg.gif) ![`](backtick.gif) ![z](_z.gif)
![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
80 | | funbrfv 5357 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
![(](lp.gif) ![(](lp.gif) ![z](_z.gif) ![G](_cg.gif) ![(](lp.gif) ![G](_cg.gif) ![`](backtick.gif) ![z](_z.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) |
81 | 4, 77, 80 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
![(](lp.gif) ![(](lp.gif) ![z](_z.gif) ![G](_cg.gif) ![(](lp.gif) ![G](_cg.gif) ![`](backtick.gif) ![z](_z.gif)
![b](_b.gif) ![)](rp.gif) ![)](rp.gif) |
82 | 79, 81 | anim12d 546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) ![G](_cg.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![G](_cg.gif) ![`](backtick.gif) ![z](_z.gif) ![(](lp.gif) ![G](_cg.gif) ![`](backtick.gif) ![z](_z.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
83 | | eqtr2 2371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![G](_cg.gif) ![`](backtick.gif) ![z](_z.gif)
![(](lp.gif) ![G](_cg.gif) ![`](backtick.gif) ![z](_z.gif) ![b](_b.gif)
![b](_b.gif) ![)](rp.gif) |
84 | 76, 82, 83 | syl56 30 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![G](_cg.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif)
![b](_b.gif) ![)](rp.gif) ![)](rp.gif) |
85 | 84 | exp3a 425 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![G](_cg.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
86 | 73, 85 | syl5 28 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif)
![z](_z.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![G](_cg.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
87 | 86 | exp3a 425 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![G](_cg.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
88 | 87 | com34 77 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![G](_cg.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
89 | 88 | imp3a 420 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![(](lp.gif) ![y](_y.gif) ![G](_cg.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
90 | 89 | com12 27 |
. . . . . . . . . . . . . . . . . . . . . . 23
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![(](lp.gif) ![y](_y.gif) ![G](_cg.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
91 | 90 | an4s 799 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![y](_y.gif) ![G](_cg.gif) ![a](_a.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
92 | 91 | com3l 75 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![y](_y.gif) ![G](_cg.gif) ![a](_a.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
93 | 92 | imp3a 420 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif)
![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![y](_y.gif) ![G](_cg.gif) ![a](_a.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) |
94 | 93 | exlimdvv 1637 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![y](_y.gif) ![G](_cg.gif) ![a](_a.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) |
95 | 94 | adantr 451 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![y](_y.gif) ![G](_cg.gif) ![a](_a.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) |
96 | 72, 95 | syl5 28 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![y](_y.gif) ![G](_cg.gif) ![a](_a.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) |
97 | 96 | exp3a 425 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif)
![z](_z.gif) ![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![y](_y.gif) ![G](_cg.gif) ![a](_a.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif)
![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
98 | 97 | impr 602 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif)
![z](_z.gif) ![)](rp.gif) ![)](rp.gif)
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![y](_y.gif) ![G](_cg.gif) ![a](_a.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![G](_cg.gif) ![b](_b.gif) ![)](rp.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) |
99 | 68, 98 | syld 40 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif)
![z](_z.gif) ![)](rp.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![b](_b.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) |
100 | 99 | alrimivv 1632 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif)
![z](_z.gif) ![)](rp.gif) ![)](rp.gif)
![A.](forall.gif) ![a](_a.gif) ![A.](forall.gif) ![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![(](lp.gif)
1c![)](rp.gif) ![F](_cf.gif) ![b](_b.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) |
101 | 100 | expr 598 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif)
![z](_z.gif) ![A.](forall.gif) ![a](_a.gif) ![A.](forall.gif) ![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c![)](rp.gif) ![F](_cf.gif)
![(](lp.gif) 1c![)](rp.gif) ![F](_cf.gif) ![b](_b.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
102 | 101 | ancoms 439 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) Nn ![ph](_varphi.gif) ![(](lp.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![F](_cf.gif) ![t](_t.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![A.](forall.gif) ![a](_a.gif) ![A.](forall.gif) ![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c![)](rp.gif) ![F](_cf.gif)
![(](lp.gif) 1c![)](rp.gif) ![F](_cf.gif) ![b](_b.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
103 | 13, 18, 23, 35, 40, 49, 102 | findsd 4411 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) Nn ![ph](_varphi.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![F](_cf.gif) ![x](_x.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
104 | 103 | 19.21bbi 1865 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Nn ![ph](_varphi.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![F](_cf.gif) ![x](_x.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
105 | 104 | ex 423 |
. . . . . . . 8
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![F](_cf.gif) ![x](_x.gif) ![F](_cf.gif) ![z](_z.gif)
![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
106 | 105 | imp3a 420 |
. . . . . . 7
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![F](_cf.gif) ![x](_x.gif) ![F](_cf.gif) ![z](_z.gif) ![)](rp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
107 | 10, 106 | mpcom 32 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![F](_cf.gif) ![x](_x.gif) ![F](_cf.gif) ![z](_z.gif) ![)](rp.gif)
![z](_z.gif) ![)](rp.gif) |
108 | 107 | ex 423 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![F](_cf.gif) ![x](_x.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
109 | 108 | alrimivv 1632 |
. . . 4
![(](lp.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![F](_cf.gif) ![x](_x.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
110 | 109 | alrimiv 1631 |
. . 3
![(](lp.gif) ![A.](forall.gif) ![x](_x.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![F](_cf.gif) ![x](_x.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
111 | | dffun2 5120 |
. . 3
![(](lp.gif) ![A.](forall.gif) ![x](_x.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![F](_cf.gif) ![x](_x.gif) ![F](_cf.gif) ![z](_z.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
112 | 110, 111 | sylibr 203 |
. 2
![(](lp.gif) ![F](_cf.gif) ![)](rp.gif) |
113 | | df-fn 4791 |
. 2
![(](lp.gif) Nn ![(](lp.gif) Nn ![)](rp.gif) ![)](rp.gif) |
114 | 112, 7, 113 | sylanbrc 645 |
1
![(](lp.gif) Nn ![)](rp.gif) |