Step | Hyp | Ref
| Expression |
1 | | sikexlem.1 |
. . 3
1c k 1c![)](rp.gif) |
2 | | sikexlem.2 |
. . 3
1c k 1c![)](rp.gif) |
3 | | ssofeq 4077 |
. . 3
![(](lp.gif) ![(](lp.gif)
1c
k
1c
1c k 1c![)](rp.gif) ![(](lp.gif) ![A.](forall.gif)
1c k
1c![)](rp.gif) ![(](lp.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
4 | 1, 2, 3 | mp2an 653 |
. 2
![(](lp.gif) ![A.](forall.gif) 1c k 1c![)](rp.gif) ![(](lp.gif)
![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
5 | | df-ral 2619 |
. . 3
![(](lp.gif) ![A.](forall.gif)
1c
k
1c![)](rp.gif) ![(](lp.gif) ![B](_cb.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) 1c k 1c ![(](lp.gif)
![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
6 | | elxpk 4196 |
. . . . . . . 8
![(](lp.gif) 1c k 1c ![E.](exists.gif) ![w](_w.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![<<](llangle.gif) ![w](_w.gif) ![t](_t.gif) ![(](lp.gif) 1c
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
7 | | el1c 4139 |
. . . . . . . . . . . . . 14
![(](lp.gif) 1c ![E.](exists.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif) |
8 | | el1c 4139 |
. . . . . . . . . . . . . 14
![(](lp.gif) 1c ![E.](exists.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) |
9 | 7, 8 | anbi12i 678 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif)
1c 1c ![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![x](_x.gif) ![E.](exists.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
10 | | eeanv 1913 |
. . . . . . . . . . . . 13
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![x](_x.gif) ![E.](exists.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
11 | 9, 10 | bitr4i 243 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif)
1c 1c ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
12 | 11 | anbi2i 675 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![w](_w.gif) ![t](_t.gif) ![(](lp.gif) 1c
1c![)](rp.gif) ![(](lp.gif) ![<<](llangle.gif) ![w](_w.gif) ![t](_t.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
13 | | df-3an 936 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![w](_w.gif) ![t](_t.gif) ![>>](rrangle.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![w](_w.gif) ![t](_t.gif) ![>>](rrangle.gif) ![)](rp.gif) ![)](rp.gif) |
14 | | ancom 437 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![w](_w.gif) ![t](_t.gif) ![>>](rrangle.gif) ![(](lp.gif) ![<<](llangle.gif) ![w](_w.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
15 | 13, 14 | bitri 240 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![w](_w.gif) ![t](_t.gif) ![>>](rrangle.gif) ![(](lp.gif) ![<<](llangle.gif) ![w](_w.gif) ![t](_t.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
16 | 15 | 2exbii 1583 |
. . . . . . . . . . . 12
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif)
![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![w](_w.gif) ![t](_t.gif) ![>>](rrangle.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif)
![<<](llangle.gif) ![w](_w.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
17 | | 19.42vv 1907 |
. . . . . . . . . . . 12
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<<](llangle.gif) ![w](_w.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![(](lp.gif) ![<<](llangle.gif) ![w](_w.gif) ![t](_t.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
18 | 16, 17 | bitri 240 |
. . . . . . . . . . 11
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif)
![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![w](_w.gif) ![t](_t.gif) ![>>](rrangle.gif) ![(](lp.gif) ![<<](llangle.gif) ![w](_w.gif) ![t](_t.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
19 | 12, 18 | bitr4i 243 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![w](_w.gif) ![t](_t.gif) ![(](lp.gif) 1c
1c![)](rp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![{](lbrace.gif) ![y](_y.gif)
![<<](llangle.gif) ![w](_w.gif) ![t](_t.gif) ![>>](rrangle.gif) ![)](rp.gif) ![)](rp.gif) |
20 | 19 | 2exbii 1583 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif) ![w](_w.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![<<](llangle.gif) ![w](_w.gif) ![t](_t.gif) ![(](lp.gif) 1c
1c![)](rp.gif) ![E.](exists.gif) ![w](_w.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![w](_w.gif) ![t](_t.gif) ![>>](rrangle.gif) ![)](rp.gif) ![)](rp.gif) |
21 | | exrot4 1745 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![w](_w.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![{](lbrace.gif) ![y](_y.gif)
![<<](llangle.gif) ![w](_w.gif) ![t](_t.gif) ![>>](rrangle.gif) ![E.](exists.gif) ![w](_w.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![w](_w.gif) ![t](_t.gif) ![>>](rrangle.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 20, 21 | bitr4i 243 |
. . . . . . . 8
![(](lp.gif) ![E.](exists.gif) ![w](_w.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![<<](llangle.gif) ![w](_w.gif) ![t](_t.gif) ![(](lp.gif) 1c
1c![)](rp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![w](_w.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![w](_w.gif) ![t](_t.gif) ![>>](rrangle.gif) ![)](rp.gif) ![)](rp.gif) |
23 | | snex 4111 |
. . . . . . . . . 10
![{](lbrace.gif) ![x](_x.gif)
![_V](rmcv.gif) |
24 | | snex 4111 |
. . . . . . . . . 10
![{](lbrace.gif) ![y](_y.gif)
![_V](rmcv.gif) |
25 | | opkeq1 4059 |
. . . . . . . . . . 11
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![w](_w.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![t](_t.gif) ![>>](rrangle.gif) ![)](rp.gif) |
26 | 25 | eqeq2d 2364 |
. . . . . . . . . 10
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![(](lp.gif) ![<<](llangle.gif) ![w](_w.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![t](_t.gif) ![>>](rrangle.gif) ![)](rp.gif) ![)](rp.gif) |
27 | | opkeq2 4060 |
. . . . . . . . . . 11
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![>>](rrangle.gif) ![)](rp.gif) |
28 | 27 | eqeq2d 2364 |
. . . . . . . . . 10
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![t](_t.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![>>](rrangle.gif) ![)](rp.gif) ![)](rp.gif) |
29 | 23, 24, 26, 28 | ceqsex2v 2896 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif) ![w](_w.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif)
![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![w](_w.gif) ![t](_t.gif) ![>>](rrangle.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![>>](rrangle.gif) ![)](rp.gif) |
30 | 29 | 2exbii 1583 |
. . . . . . . 8
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![w](_w.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![{](lbrace.gif) ![y](_y.gif)
![<<](llangle.gif) ![w](_w.gif) ![t](_t.gif) ![>>](rrangle.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![>>](rrangle.gif) ![)](rp.gif) |
31 | 6, 22, 30 | 3bitri 262 |
. . . . . . 7
![(](lp.gif) 1c k 1c ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![>>](rrangle.gif) ![)](rp.gif) |
32 | 31 | imbi1i 315 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) 1c k
1c
![(](lp.gif)
![B](_cb.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif)
![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
33 | | 19.23vv 1892 |
. . . . . 6
![(](lp.gif) ![A.](forall.gif) ![x](_x.gif) ![A.](forall.gif) ![y](_y.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif)
![B](_cb.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
34 | 32, 33 | bitr4i 243 |
. . . . 5
![(](lp.gif) ![(](lp.gif) 1c k
1c
![(](lp.gif)
![B](_cb.gif) ![)](rp.gif) ![A.](forall.gif) ![x](_x.gif) ![A.](forall.gif) ![y](_y.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif)
![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
35 | 34 | albii 1566 |
. . . 4
![(](lp.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) 1c k 1c ![(](lp.gif)
![B](_cb.gif) ![)](rp.gif) ![A.](forall.gif) ![z](_z.gif) ![A.](forall.gif) ![x](_x.gif) ![A.](forall.gif) ![y](_y.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![(](lp.gif)
![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
36 | | alrot3 1738 |
. . . 4
![(](lp.gif) ![A.](forall.gif) ![z](_z.gif) ![A.](forall.gif) ![x](_x.gif) ![A.](forall.gif) ![y](_y.gif) ![(](lp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif) ![B](_cb.gif) ![)](rp.gif) ![A.](forall.gif) ![x](_x.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
37 | 35, 36 | bitri 240 |
. . 3
![(](lp.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) 1c k 1c ![(](lp.gif)
![B](_cb.gif) ![)](rp.gif) ![A.](forall.gif) ![x](_x.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![(](lp.gif)
![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
38 | | opkex 4113 |
. . . . 5
![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
39 | | eleq1 2413 |
. . . . . 6
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
40 | | eleq1 2413 |
. . . . . 6
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
41 | 39, 40 | bibi12d 312 |
. . . . 5
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif)
![B](_cb.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
42 | 38, 41 | ceqsalv 2885 |
. . . 4
![(](lp.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![(](lp.gif)
![B](_cb.gif) ![)](rp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
43 | 42 | 2albii 1567 |
. . 3
![(](lp.gif) ![A.](forall.gif) ![x](_x.gif) ![A.](forall.gif) ![y](_y.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif) ![B](_cb.gif) ![)](rp.gif) ![A.](forall.gif) ![x](_x.gif) ![A.](forall.gif) ![y](_y.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
44 | 5, 37, 43 | 3bitri 262 |
. 2
![(](lp.gif) ![A.](forall.gif)
1c
k
1c![)](rp.gif) ![(](lp.gif) ![B](_cb.gif) ![A.](forall.gif) ![x](_x.gif) ![A.](forall.gif) ![y](_y.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
45 | 4, 44 | bitri 240 |
1
![(](lp.gif) ![A.](forall.gif) ![x](_x.gif) ![A.](forall.gif) ![y](_y.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |