Step | Hyp | Ref
| Expression |
1 | | df-mpt 5652 |
. . 3
![(](lp.gif) ![(](lp.gif) ![G](_cg.gif)
![(](lp.gif) ![s](_s.gif) ![)](rp.gif) ![{](lbrace.gif) ![<.](langle.gif) ![s](_s.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![G](_cg.gif) ![(](lp.gif) ![s](_s.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) |
2 | | enmap1lem1.1 |
. . 3
![(](lp.gif)
![(](lp.gif) ![G](_cg.gif) ![(](lp.gif) ![s](_s.gif) ![)](rp.gif) ![)](rp.gif) |
3 | | opelres 4950 |
. . . . 5
![(](lp.gif) ![<.](langle.gif) ![s](_s.gif)
![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif)
![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) Compose
![(](lp.gif) ![G](_cg.gif) ![)](rp.gif) ![(](lp.gif) ![<.](langle.gif) ![s](_s.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![1st](_1st.gif)
![2nd](_2nd.gif) ![)](rp.gif) Compose
![(](lp.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
4 | | elima 4754 |
. . . . . . . . 9
![(](lp.gif) ![<.](langle.gif) ![s](_s.gif)
![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) Compose ![E.](exists.gif) Compose ![p](_p.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![1st](_1st.gif)
![2nd](_2nd.gif) ![)](rp.gif) ![<.](langle.gif) ![s](_s.gif) ![x](_x.gif) ![>.](rangle.gif) ![)](rp.gif) |
5 | | trtxp 5781 |
. . . . . . . . . . . 12
![(](lp.gif) ![p](_p.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![1st](_1st.gif)
![2nd](_2nd.gif) ![)](rp.gif) ![<.](langle.gif) ![s](_s.gif) ![x](_x.gif) ![(](lp.gif) ![p](_p.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![1st](_1st.gif) ![)](rp.gif) ![p](_p.gif) ![2nd](_2nd.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
6 | | brco 4883 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![p](_p.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![1st](_1st.gif) ![)](rp.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![p](_p.gif) ![1st](_1st.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![s](_s.gif) ![)](rp.gif) ![)](rp.gif) |
7 | | ancom 437 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![p](_p.gif) ![1st](_1st.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![s](_s.gif) ![(](lp.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![p](_p.gif) ![1st](_1st.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
8 | | brin 4693 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![(](lp.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) ![x](_x.gif) ![2nd](_2nd.gif) ![s](_s.gif) ![)](rp.gif) ![)](rp.gif) |
9 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . 21
![_V](rmcv.gif) |
10 | | brxp 4812 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif)
![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
11 | 9, 10 | mpbiran2 885 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
12 | | eliniseg 5020 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![x](_x.gif) ![1st](_1st.gif) ![r](_r.gif) ![)](rp.gif) |
13 | 11, 12 | bitri 240 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) ![x](_x.gif) ![1st](_1st.gif) ![r](_r.gif) ![)](rp.gif) |
14 | 13 | anbi1i 676 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![)](rp.gif) ![x](_x.gif) ![2nd](_2nd.gif) ![s](_s.gif) ![(](lp.gif) ![x](_x.gif) ![1st](_1st.gif) ![x](_x.gif) ![2nd](_2nd.gif) ![s](_s.gif) ![)](rp.gif) ![)](rp.gif) |
15 | | vex 2862 |
. . . . . . . . . . . . . . . . . . 19
![_V](rmcv.gif) |
16 | 15, 9 | op1st2nd 5790 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![1st](_1st.gif) ![x](_x.gif) ![2nd](_2nd.gif) ![s](_s.gif) ![<.](langle.gif) ![r](_r.gif) ![s](_s.gif) ![>.](rangle.gif) ![)](rp.gif) |
17 | 8, 14, 16 | 3bitri 262 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![<.](langle.gif) ![r](_r.gif) ![s](_s.gif) ![>.](rangle.gif) ![)](rp.gif) |
18 | 17 | anbi1i 676 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![p](_p.gif) ![1st](_1st.gif) ![x](_x.gif) ![(](lp.gif) ![<.](langle.gif) ![r](_r.gif)
![s](_s.gif) ![p](_p.gif) ![1st](_1st.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
19 | 7, 18 | bitri 240 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![p](_p.gif) ![1st](_1st.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![s](_s.gif) ![(](lp.gif) ![<.](langle.gif) ![r](_r.gif) ![s](_s.gif) ![p](_p.gif) ![1st](_1st.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
20 | 19 | exbii 1582 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![p](_p.gif) ![1st](_1st.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![s](_s.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![<.](langle.gif) ![r](_r.gif) ![s](_s.gif) ![p](_p.gif) ![1st](_1st.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
21 | 15, 9 | opex 4588 |
. . . . . . . . . . . . . . 15
![<.](langle.gif) ![r](_r.gif) ![s](_s.gif) ![_V](rmcv.gif) |
22 | | breq2 4643 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![<.](langle.gif) ![r](_r.gif) ![s](_s.gif) ![(](lp.gif) ![p](_p.gif) ![1st](_1st.gif) ![p](_p.gif) ![1st](_1st.gif) ![<.](langle.gif) ![r](_r.gif) ![s](_s.gif) ![>.](rangle.gif) ![)](rp.gif) ![)](rp.gif) |
23 | 21, 22 | ceqsexv 2894 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![<.](langle.gif) ![r](_r.gif)
![s](_s.gif) ![p](_p.gif) ![1st](_1st.gif) ![x](_x.gif) ![p](_p.gif) ![1st](_1st.gif) ![<.](langle.gif) ![r](_r.gif) ![s](_s.gif) ![>.](rangle.gif) ![)](rp.gif) |
24 | 6, 20, 23 | 3bitri 262 |
. . . . . . . . . . . . 13
![(](lp.gif) ![p](_p.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![1st](_1st.gif) ![)](rp.gif) ![p](_p.gif) ![1st](_1st.gif) ![<.](langle.gif) ![r](_r.gif) ![s](_s.gif) ![>.](rangle.gif) ![)](rp.gif) |
25 | 24 | anbi1i 676 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![p](_p.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![1st](_1st.gif) ![)](rp.gif) ![p](_p.gif) ![2nd](_2nd.gif) ![x](_x.gif) ![(](lp.gif) ![p](_p.gif) ![1st](_1st.gif) ![<.](langle.gif) ![r](_r.gif) ![s](_s.gif) ![p](_p.gif) ![2nd](_2nd.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
26 | | vex 2862 |
. . . . . . . . . . . . 13
![_V](rmcv.gif) |
27 | 21, 26 | op1st2nd 5790 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![p](_p.gif) ![1st](_1st.gif) ![<.](langle.gif) ![r](_r.gif) ![s](_s.gif) ![p](_p.gif) ![2nd](_2nd.gif) ![x](_x.gif) ![<.](langle.gif) ![<.](langle.gif) ![r](_r.gif) ![s](_s.gif) ![>.](rangle.gif) ![x](_x.gif) ![>.](rangle.gif) ![)](rp.gif) |
28 | 5, 25, 27 | 3bitri 262 |
. . . . . . . . . . 11
![(](lp.gif) ![p](_p.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![1st](_1st.gif)
![2nd](_2nd.gif) ![)](rp.gif) ![<.](langle.gif) ![s](_s.gif) ![x](_x.gif) ![<.](langle.gif) ![<.](langle.gif) ![r](_r.gif) ![s](_s.gif) ![>.](rangle.gif) ![x](_x.gif) ![>.](rangle.gif) ![)](rp.gif) |
29 | 28 | rexbii 2639 |
. . . . . . . . . 10
![(](lp.gif) ![E.](exists.gif)
Compose ![p](_p.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![1st](_1st.gif)
![2nd](_2nd.gif) ![)](rp.gif) ![<.](langle.gif) ![s](_s.gif) ![x](_x.gif) ![E.](exists.gif) Compose ![<.](langle.gif) ![<.](langle.gif) ![r](_r.gif) ![s](_s.gif) ![>.](rangle.gif) ![x](_x.gif) ![>.](rangle.gif) ![)](rp.gif) |
30 | | risset 2661 |
. . . . . . . . . 10
![(](lp.gif) ![<.](langle.gif) ![<.](langle.gif) ![r](_r.gif) ![s](_s.gif) ![>.](rangle.gif) ![x](_x.gif) Compose ![E.](exists.gif) Compose ![<.](langle.gif) ![<.](langle.gif) ![r](_r.gif) ![s](_s.gif) ![>.](rangle.gif) ![x](_x.gif) ![>.](rangle.gif) ![)](rp.gif) |
31 | 29, 30 | bitr4i 243 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif)
Compose ![p](_p.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![1st](_1st.gif)
![2nd](_2nd.gif) ![)](rp.gif) ![<.](langle.gif) ![s](_s.gif) ![x](_x.gif) ![<.](langle.gif) ![<.](langle.gif) ![r](_r.gif) ![s](_s.gif) ![>.](rangle.gif) ![x](_x.gif) Compose ![)](rp.gif) |
32 | 4, 31 | bitri 240 |
. . . . . . . 8
![(](lp.gif) ![<.](langle.gif) ![s](_s.gif)
![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) Compose ![<.](langle.gif) ![<.](langle.gif) ![r](_r.gif) ![s](_s.gif) ![>.](rangle.gif) ![x](_x.gif) Compose ![)](rp.gif) |
33 | | df-br 4640 |
. . . . . . . 8
![(](lp.gif) ![<.](langle.gif) ![r](_r.gif)
![s](_s.gif) Compose
![<.](langle.gif) ![<.](langle.gif) ![r](_r.gif) ![s](_s.gif) ![>.](rangle.gif) ![x](_x.gif) Compose ![)](rp.gif) |
34 | 32, 33 | bitr4i 243 |
. . . . . . 7
![(](lp.gif) ![<.](langle.gif) ![s](_s.gif)
![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) Compose ![<.](langle.gif) ![r](_r.gif) ![s](_s.gif)
Compose ![x](_x.gif) ![)](rp.gif) |
35 | | brcomposeg 5819 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif)
![_V](rmcv.gif) ![(](lp.gif) ![<.](langle.gif) ![r](_r.gif) ![s](_s.gif)
Compose ![(](lp.gif) ![s](_s.gif)
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
36 | 15, 9, 35 | mp2an 653 |
. . . . . . 7
![(](lp.gif) ![<.](langle.gif) ![r](_r.gif)
![s](_s.gif) Compose
![(](lp.gif) ![s](_s.gif) ![x](_x.gif) ![)](rp.gif) |
37 | | eqcom 2355 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![s](_s.gif) ![(](lp.gif) ![s](_s.gif) ![)](rp.gif) ![)](rp.gif) |
38 | 34, 36, 37 | 3bitri 262 |
. . . . . 6
![(](lp.gif) ![<.](langle.gif) ![s](_s.gif)
![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) Compose ![(](lp.gif) ![s](_s.gif) ![)](rp.gif) ![)](rp.gif) |
39 | 38 | anbi2ci 677 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![<.](langle.gif) ![s](_s.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) Compose ![(](lp.gif) ![G](_cg.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![G](_cg.gif) ![(](lp.gif) ![s](_s.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
40 | 3, 39 | bitri 240 |
. . . 4
![(](lp.gif) ![<.](langle.gif) ![s](_s.gif)
![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif)
![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) Compose
![(](lp.gif) ![G](_cg.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![G](_cg.gif)
![(](lp.gif) ![s](_s.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
41 | 40 | opabbi2i 4866 |
. . 3
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![1st](_1st.gif)
![2nd](_2nd.gif) ![)](rp.gif) Compose ![(](lp.gif)
![G](_cg.gif) ![)](rp.gif) ![{](lbrace.gif) ![<.](langle.gif) ![s](_s.gif)
![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![G](_cg.gif)
![(](lp.gif) ![s](_s.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) |
42 | 1, 2, 41 | 3eqtr4i 2383 |
. 2
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) Compose
![(](lp.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) |
43 | | 1stex 4739 |
. . . . . . . . . 10
![_V](rmcv.gif) |
44 | 43 | cnvex 5102 |
. . . . . . . . 9
![`'](_cnv.gif) ![_V](rmcv.gif) |
45 | | snex 4111 |
. . . . . . . . 9
![{](lbrace.gif) ![r](_r.gif)
![_V](rmcv.gif) |
46 | 44, 45 | imaex 4747 |
. . . . . . . 8
![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif)
![_V](rmcv.gif) |
47 | | vvex 4109 |
. . . . . . . 8
![_V](rmcv.gif) |
48 | 46, 47 | xpex 5115 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif)
![_V](rmcv.gif) |
49 | | 2ndex 5112 |
. . . . . . 7
![_V](rmcv.gif) |
50 | 48, 49 | inex 4105 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![_V](rmcv.gif) |
51 | 50, 43 | coex 4750 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![1st](_1st.gif) ![_V](rmcv.gif) |
52 | 51, 49 | txpex 5785 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif)
![1st](_1st.gif) ![2nd](_2nd.gif) ![_V](rmcv.gif) |
53 | | composeex 5820 |
. . . 4
Compose ![_V](rmcv.gif) |
54 | 52, 53 | imaex 4747 |
. . 3
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![1st](_1st.gif)
![2nd](_2nd.gif) ![)](rp.gif) Compose ![_V](rmcv.gif) |
55 | | ovex 5551 |
. . 3
![(](lp.gif) ![G](_cg.gif) ![_V](rmcv.gif) |
56 | 54, 55 | resex 5117 |
. 2
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![1st](_1st.gif) !["](backquote.gif) ![{](lbrace.gif) ![r](_r.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![2nd](_2nd.gif) ![1st](_1st.gif)
![2nd](_2nd.gif) ![)](rp.gif) Compose ![(](lp.gif)
![G](_cg.gif) ![)](rp.gif) ![_V](rmcv.gif) |
57 | 42, 56 | eqeltri 2423 |
1
![_V](rmcv.gif) |