Step | Hyp | Ref
| Expression |
1 | | vex 2862 |
. . . . . . . 8
![_V](rmcv.gif) |
2 | 1 | elcompl 3225 |
. . . . . . 7
![(](lp.gif) ∼ ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Nn ![)](rp.gif) ![)](rp.gif) |
3 | | elima 4754 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Nn ![E.](exists.gif) Nn ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif)
![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![a](_a.gif) ![)](rp.gif) |
4 | | df-br 4640 |
. . . . . . . . . . 11
![(](lp.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif)
![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
5 | | elrn 4896 |
. . . . . . . . . . . 12
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![a](_a.gif) ![(](lp.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif)
![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![p](_p.gif) ![(](lp.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif)
![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) ![>.](rangle.gif) ![)](rp.gif) |
6 | | df-br 4640 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![p](_p.gif) ![(](lp.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif)
![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) ![<.](langle.gif) ![p](_p.gif) ![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) ![>.](rangle.gif) ![(](lp.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif)
![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
7 | | oteltxp 5782 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![<.](langle.gif) ![p](_p.gif)
![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) ![>.](rangle.gif) ![(](lp.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![<.](langle.gif) ![p](_p.gif)
![n](_n.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![<.](langle.gif) ![p](_p.gif)
![a](_a.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
8 | 6, 7 | bitri 240 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![p](_p.gif) ![(](lp.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif)
![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) ![(](lp.gif) ![<.](langle.gif) ![p](_p.gif) ![n](_n.gif) ![(](lp.gif)
AddC ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif)
![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![<.](langle.gif) ![p](_p.gif) ![a](_a.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
9 | | elrn2 4897 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![<.](langle.gif) ![p](_p.gif)
![n](_n.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![q](_q.gif) ![<.](langle.gif) ![q](_q.gif) ![<.](langle.gif) ![p](_p.gif) ![n](_n.gif) ![>.](rangle.gif) ![(](lp.gif)
AddC ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif)
![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
10 | | oteltxp 5782 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![<.](langle.gif) ![q](_q.gif)
![<.](langle.gif) ![p](_p.gif) ![n](_n.gif) ![>.](rangle.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif)
![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![<.](langle.gif) ![q](_q.gif) ![p](_p.gif) AddC ![`'](_cnv.gif) ![(](lp.gif)
![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![<.](langle.gif) ![q](_q.gif) ![n](_n.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif)
![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
11 | | opelco 4884 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![<.](langle.gif) ![q](_q.gif)
![p](_p.gif)
AddC ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif)
![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![q](_q.gif) ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) AddC ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
12 | | brcnv 4892 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) ![q](_q.gif) ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif)
![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![q](_q.gif) ![)](rp.gif) |
13 | | brres 4949 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif)
![(](lp.gif) ![x](_x.gif) ![1st](_1st.gif)
![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
14 | 12, 13 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![q](_q.gif) ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif)
![(](lp.gif) ![x](_x.gif) ![1st](_1st.gif)
![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
15 | | eliniseg 5020 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![x](_x.gif) 1c![)](rp.gif) |
16 | 15 | anbi2i 675 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![1st](_1st.gif)
![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![(](lp.gif) ![x](_x.gif) ![1st](_1st.gif)
![x](_x.gif) 1c![)](rp.gif) ![)](rp.gif) |
17 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![_V](rmcv.gif) |
18 | | 1cex 4142 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
1c
![_V](rmcv.gif) |
19 | 17, 18 | op1st2nd 5790 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![(](lp.gif) ![x](_x.gif) ![1st](_1st.gif) ![x](_x.gif) 1c ![<.](langle.gif) ![q](_q.gif)
1c![>.](rangle.gif) ![)](rp.gif) |
20 | 14, 16, 19 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . 23
![(](lp.gif) ![q](_q.gif) ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif)
![<.](langle.gif) ![q](_q.gif)
1c![>.](rangle.gif) ![)](rp.gif) |
21 | 20 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![(](lp.gif) ![q](_q.gif) ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) AddC ![p](_p.gif) ![(](lp.gif) ![<.](langle.gif) ![q](_q.gif)
1c AddC ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 21 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![q](_q.gif) ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif)
AddC ![p](_p.gif)
![E.](exists.gif) ![x](_x.gif) ![(](lp.gif)
![<.](langle.gif) ![q](_q.gif)
1c AddC ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
23 | 17, 18 | opex 4588 |
. . . . . . . . . . . . . . . . . . . . . 22
![<.](langle.gif) ![q](_q.gif) 1c ![_V](rmcv.gif) |
24 | | breq1 4642 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![<.](langle.gif) ![q](_q.gif) 1c ![(](lp.gif) AddC ![<.](langle.gif) ![q](_q.gif) 1c AddC
![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
25 | 23, 24 | ceqsexv 2894 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![<.](langle.gif) ![q](_q.gif)
1c AddC ![p](_p.gif) ![<.](langle.gif) ![q](_q.gif) 1c AddC ![p](_p.gif) ![)](rp.gif) |
26 | 22, 25 | bitri 240 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![q](_q.gif) ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif)
AddC ![p](_p.gif)
![<.](langle.gif) ![q](_q.gif) 1c AddC
![p](_p.gif) ![)](rp.gif) |
27 | 17, 18 | braddcfn 5826 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![<.](langle.gif) ![q](_q.gif)
1c AddC ![(](lp.gif)
1c
![p](_p.gif) ![)](rp.gif) |
28 | | eqcom 2355 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
29 | 27, 28 | bitri 240 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![<.](langle.gif) ![q](_q.gif)
1c AddC ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
30 | 11, 26, 29 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![<.](langle.gif) ![q](_q.gif)
![p](_p.gif)
AddC ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif)
![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) |
31 | | opelcnv 4893 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![<.](langle.gif) ![q](_q.gif)
![n](_n.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![<.](langle.gif) ![n](_n.gif) ![q](_q.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
32 | | nncdiv3lem1 6275 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![q](_q.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
33 | 31, 32 | bitri 240 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![<.](langle.gif) ![q](_q.gif)
![n](_n.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
34 | 30, 33 | anbi12i 678 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![<.](langle.gif) ![q](_q.gif) ![p](_p.gif)
AddC ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif)
![<.](langle.gif) ![q](_q.gif) ![n](_n.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) 1c
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
35 | | ancom 437 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
36 | 10, 34, 35 | 3bitri 262 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![<.](langle.gif) ![q](_q.gif)
![<.](langle.gif) ![p](_p.gif) ![n](_n.gif) ![>.](rangle.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif)
![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
37 | 36 | exbii 1582 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![E.](exists.gif) ![q](_q.gif) ![<.](langle.gif) ![q](_q.gif) ![<.](langle.gif) ![p](_p.gif)
![n](_n.gif) ![>.](rangle.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![q](_q.gif) ![(](lp.gif)
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif)
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
38 | | vex 2862 |
. . . . . . . . . . . . . . . . . . 19
![_V](rmcv.gif) |
39 | 38, 38 | addcex 4394 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![n](_n.gif) ![_V](rmcv.gif) |
40 | 39, 38 | addcex 4394 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![_V](rmcv.gif) |
41 | | addceq1 4383 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
42 | 41 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
43 | 40, 42 | ceqsexv 2894 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![E.](exists.gif) ![q](_q.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
![(](lp.gif) 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
44 | 9, 37, 43 | 3bitri 262 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![<.](langle.gif) ![p](_p.gif)
![n](_n.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
45 | | opelcnv 4893 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![<.](langle.gif) ![p](_p.gif)
![a](_a.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![<.](langle.gif) ![a](_a.gif) ![p](_p.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
46 | | nncdiv3lem1 6275 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![<.](langle.gif) ![a](_a.gif)
![p](_p.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![a](_a.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
47 | 45, 46 | bitri 240 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![<.](langle.gif) ![p](_p.gif)
![a](_a.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![a](_a.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
48 | 44, 47 | anbi12i 678 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![<.](langle.gif) ![p](_p.gif) ![n](_n.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![<.](langle.gif) ![p](_p.gif)
![a](_a.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![a](_a.gif)
![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
49 | | ancom 437 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c
![(](lp.gif) ![(](lp.gif)
![a](_a.gif) ![a](_a.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![a](_a.gif) ![a](_a.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
50 | 8, 48, 49 | 3bitri 262 |
. . . . . . . . . . . . 13
![(](lp.gif) ![p](_p.gif) ![(](lp.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif)
![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![a](_a.gif)
![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
51 | 50 | exbii 1582 |
. . . . . . . . . . . 12
![(](lp.gif) ![E.](exists.gif) ![p](_p.gif) ![(](lp.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif)
![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![<.](langle.gif) ![n](_n.gif) ![a](_a.gif) ![E.](exists.gif) ![p](_p.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![a](_a.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
52 | 1, 1 | addcex 4394 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![a](_a.gif) ![_V](rmcv.gif) |
53 | 52, 1 | addcex 4394 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![a](_a.gif) ![a](_a.gif) ![_V](rmcv.gif) |
54 | | eqeq1 2359 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![a](_a.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![a](_a.gif) ![a](_a.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
55 | 53, 54 | ceqsexv 2894 |
. . . . . . . . . . . 12
![(](lp.gif) ![E.](exists.gif) ![p](_p.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![a](_a.gif) ![a](_a.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![a](_a.gif)
![a](_a.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
56 | 5, 51, 55 | 3bitri 262 |
. . . . . . . . . . 11
![(](lp.gif) ![<.](langle.gif) ![n](_n.gif)
![a](_a.gif) ![(](lp.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif)
![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![a](_a.gif) ![a](_a.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
57 | 4, 56 | bitri 240 |
. . . . . . . . . 10
![(](lp.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif)
![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![a](_a.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
58 | 57 | rexbii 2639 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif)
Nn ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![a](_a.gif)
![a](_a.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
59 | | dfrex2 2627 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![a](_a.gif)
![a](_a.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![a](_a.gif) ![a](_a.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
60 | 3, 58, 59 | 3bitrri 263 |
. . . . . . . 8
![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![a](_a.gif) ![a](_a.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Nn ![)](rp.gif) ![)](rp.gif) |
61 | 60 | con1bii 321 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif)
![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif)
![a](_a.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
62 | 2, 61 | bitri 240 |
. . . . . 6
![(](lp.gif) ∼ ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![a](_a.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
63 | 62 | abbi2i 2464 |
. . . . 5
∼ ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif)
![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Nn ![{](lbrace.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![a](_a.gif) ![a](_a.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![}](rbrace.gif) |
64 | | addcfnex 5824 |
. . . . . . . . . . . 12
AddC ![_V](rmcv.gif) |
65 | | 1stex 4739 |
. . . . . . . . . . . . . 14
![_V](rmcv.gif) |
66 | | 2ndex 5112 |
. . . . . . . . . . . . . . . 16
![_V](rmcv.gif) |
67 | 66 | cnvex 5102 |
. . . . . . . . . . . . . . 15
![`'](_cnv.gif) ![_V](rmcv.gif) |
68 | | snex 4111 |
. . . . . . . . . . . . . . 15
1c ![_V](rmcv.gif) |
69 | 67, 68 | imaex 4747 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![_V](rmcv.gif) |
70 | 65, 69 | resex 5117 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif)
![_V](rmcv.gif) |
71 | 70 | cnvex 5102 |
. . . . . . . . . . . 12
![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![_V](rmcv.gif) |
72 | 64, 71 | coex 4750 |
. . . . . . . . . . 11
AddC ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![_V](rmcv.gif) |
73 | 65 | cnvex 5102 |
. . . . . . . . . . . . . . . . . . . 20
![`'](_cnv.gif) ![_V](rmcv.gif) |
74 | 65, 66 | inex 4105 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![2nd](_2nd.gif) ![_V](rmcv.gif) |
75 | 73, 74 | txpex 5785 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![_V](rmcv.gif) |
76 | 75 | rnex 5107 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![_V](rmcv.gif) |
77 | 76, 66 | txpex 5785 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![_V](rmcv.gif) |
78 | 77, 64 | imaex 4747 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![_V](rmcv.gif) |
79 | 78 | cnvex 5102 |
. . . . . . . . . . . . . . 15
![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif)
![2nd](_2nd.gif) ![)](rp.gif) AddC ![_V](rmcv.gif) |
80 | 79 | ins3ex 5798 |
. . . . . . . . . . . . . 14
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![_V](rmcv.gif) |
81 | 65, 65 | coex 4750 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![1st](_1st.gif) ![_V](rmcv.gif) |
82 | 66, 65 | coex 4750 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![1st](_1st.gif) ![_V](rmcv.gif) |
83 | 82, 66 | txpex 5785 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![_V](rmcv.gif) |
84 | 81, 83 | txpex 5785 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![_V](rmcv.gif) |
85 | 84, 64 | imaex 4747 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![_V](rmcv.gif) |
86 | 80, 85 | inex 4105 |
. . . . . . . . . . . . 13
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![_V](rmcv.gif) |
87 | 86 | rnex 5107 |
. . . . . . . . . . . 12
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif)
![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![_V](rmcv.gif) |
88 | 87 | cnvex 5102 |
. . . . . . . . . . 11
![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![_V](rmcv.gif) |
89 | 72, 88 | txpex 5785 |
. . . . . . . . . 10
![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif)
![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![_V](rmcv.gif) |
90 | 89 | rnex 5107 |
. . . . . . . . 9
![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif)
![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![_V](rmcv.gif) |
91 | 90, 88 | txpex 5785 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![_V](rmcv.gif) |
92 | 91 | rnex 5107 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif)
Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![_V](rmcv.gif) |
93 | | nncex 4396 |
. . . . . . 7
Nn ![_V](rmcv.gif) |
94 | 92, 93 | imaex 4747 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif)
![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Nn ![_V](rmcv.gif) |
95 | 94 | complex 4104 |
. . . . 5
∼ ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) AddC ![`'](_cnv.gif) ![(](lp.gif)
![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 1c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![`'](_cnv.gif) Ins3 ![`'](_cnv.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![(](lp.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![2nd](_2nd.gif) ![)](rp.gif) AddC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![(](lp.gif) ![(](lp.gif) ![1st](_1st.gif) ![2nd](_2nd.gif) ![)](rp.gif) ![)](rp.gif) AddC ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Nn ![_V](rmcv.gif) |
96 | 63, 95 | eqeltrri 2424 |
. . . 4
![{](lbrace.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![a](_a.gif) ![a](_a.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif)
![_V](rmcv.gif) |
97 | | addceq12 4385 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif)
0c 0c ![(](lp.gif)
![a](_a.gif)
0c
0c![)](rp.gif) ![)](rp.gif) |
98 | 97 | anidms 626 |
. . . . . . . . 9
![(](lp.gif) 0c ![(](lp.gif) ![a](_a.gif)
0c
0c![)](rp.gif) ![)](rp.gif) |
99 | | id 19 |
. . . . . . . . 9
![(](lp.gif) 0c
0c![)](rp.gif) |
100 | 98, 99 | addceq12d 4391 |
. . . . . . . 8
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![a](_a.gif)
![a](_a.gif)
![(](lp.gif) 0c 0c 0c![)](rp.gif) ![)](rp.gif) |
101 | | addcid1 4405 |
. . . . . . . . 9
![(](lp.gif) 0c 0c 0c
0c
0c![)](rp.gif) |
102 | | addcid2 4407 |
. . . . . . . . 9
0c
0c
0c |
103 | 101, 102 | eqtri 2373 |
. . . . . . . 8
![(](lp.gif) 0c 0c 0c
0c |
104 | 100, 103 | syl6eq 2401 |
. . . . . . 7
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![a](_a.gif)
![a](_a.gif)
0c![)](rp.gif) |
105 | 104 | eqeq1d 2361 |
. . . . . 6
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![a](_a.gif) ![a](_a.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
106 | 105 | notbid 285 |
. . . . 5
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![a](_a.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c
0c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
107 | 106 | ralbidv 2634 |
. . . 4
![(](lp.gif) 0c ![(](lp.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif)
![a](_a.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![A.](forall.gif) Nn 0c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
108 | | addceq12 4385 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif)
![m](_m.gif) ![(](lp.gif) ![a](_a.gif)
![(](lp.gif) ![m](_m.gif) ![)](rp.gif) ![)](rp.gif) |
109 | 108 | anidms 626 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![a](_a.gif) ![(](lp.gif) ![m](_m.gif) ![)](rp.gif) ![)](rp.gif) |
110 | | id 19 |
. . . . . . . 8
![(](lp.gif) ![m](_m.gif) ![)](rp.gif) |
111 | 109, 110 | addceq12d 4391 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![a](_a.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
![m](_m.gif) ![)](rp.gif) ![)](rp.gif) |
112 | 111 | eqeq1d 2361 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![a](_a.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) ![m](_m.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
113 | 112 | notbid 285 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![a](_a.gif)
![a](_a.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
![m](_m.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
114 | 113 | ralbidv 2634 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![a](_a.gif) ![a](_a.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) ![m](_m.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
115 | | addceq12 4385 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
116 | 115 | anidms 626 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![a](_a.gif)
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
117 | | id 19 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
118 | 116, 117 | addceq12d 4391 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![a](_a.gif)
![a](_a.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
119 | 118 | eqeq1d 2361 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![a](_a.gif) ![a](_a.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
120 | 119 | notbid 285 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![a](_a.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
121 | 120 | ralbidv 2634 |
. . . . 5
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif)
![a](_a.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
122 | | addceq12 4385 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif)
![p](_p.gif) ![(](lp.gif) ![n](_n.gif)
![(](lp.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
123 | 122 | anidms 626 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![(](lp.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
124 | | id 19 |
. . . . . . . . . 10
![(](lp.gif) ![p](_p.gif) ![)](rp.gif) |
125 | 123, 124 | addceq12d 4391 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
126 | 125 | addceq1d 4389 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif) ![p](_p.gif) 1c![)](rp.gif) ![)](rp.gif) |
127 | 126 | eqeq2d 2364 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![p](_p.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
128 | 127 | notbid 285 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![p](_p.gif) ![p](_p.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
129 | 128 | cbvralv 2835 |
. . . . 5
![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![p](_p.gif) 1c![)](rp.gif) ![)](rp.gif) |
130 | 121, 129 | syl6bb 252 |
. . . 4
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif)
![a](_a.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![p](_p.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
131 | | addceq12 4385 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif)
![A](_ca.gif) ![(](lp.gif) ![a](_a.gif)
![(](lp.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
132 | 131 | anidms 626 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![a](_a.gif) ![(](lp.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
133 | | id 19 |
. . . . . . . 8
![(](lp.gif) ![A](_ca.gif) ![)](rp.gif) |
134 | 132, 133 | addceq12d 4391 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![a](_a.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![A](_ca.gif)
![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
135 | 134 | eqeq1d 2361 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![a](_a.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![A](_ca.gif) ![A](_ca.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
136 | 135 | notbid 285 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![a](_a.gif)
![a](_a.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![A](_ca.gif)
![A](_ca.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
137 | 136 | ralbidv 2634 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![a](_a.gif) ![a](_a.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![A](_ca.gif) ![A](_ca.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
138 | | 1ne0c 6241 |
. . . . . . . 8
1c 0c |
139 | | df-ne 2518 |
. . . . . . . 8
1c 0c
1c
0c![)](rp.gif) |
140 | 138, 139 | mpbi 199 |
. . . . . . 7
1c
0c |
141 | 140 | intnan 880 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 0c 1c 0c![)](rp.gif) |
142 | | eqcom 2355 |
. . . . . . 7
0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c
0c![)](rp.gif) |
143 | | nncaddccl 4419 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![n](_n.gif) Nn ![)](rp.gif) |
144 | 143 | anidms 626 |
. . . . . . . . . 10
![(](lp.gif) Nn ![(](lp.gif) ![n](_n.gif)
Nn ![)](rp.gif) |
145 | | nncaddccl 4419 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
Nn
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Nn ![)](rp.gif) |
146 | 144, 145 | mpancom 650 |
. . . . . . . . 9
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif)
Nn ![)](rp.gif) |
147 | | nnnc 6146 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Nn ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) NC ![)](rp.gif) |
148 | 146, 147 | syl 15 |
. . . . . . . 8
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif)
NC ![)](rp.gif) |
149 | | 1cnc 6139 |
. . . . . . . 8
1c
NC |
150 | | addceq0 6219 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif)
NC 1c NC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c
0c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 0c 1c 0c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
151 | 148, 149,
150 | sylancl 643 |
. . . . . . 7
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c
0c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 0c 1c 0c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
152 | 142, 151 | syl5bb 248 |
. . . . . 6
![(](lp.gif) Nn 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 0c 1c 0c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
153 | 141, 152 | mtbiri 294 |
. . . . 5
![(](lp.gif) Nn 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c![)](rp.gif) ![)](rp.gif) |
154 | 153 | rgen 2679 |
. . . 4
![A.](forall.gif) Nn 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c![)](rp.gif) |
155 | | nnc0suc 4412 |
. . . . . . 7
![(](lp.gif) Nn ![(](lp.gif)
0c ![E.](exists.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
156 | | 0cnsuc 4401 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![m](_m.gif) ![m](_m.gif) 1c
0c |
157 | | df-ne 2518 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![m](_m.gif) ![m](_m.gif)
1c
0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![m](_m.gif) ![m](_m.gif) 1c 0c![)](rp.gif) |
158 | 156, 157 | mpbi 199 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![m](_m.gif) ![m](_m.gif) 1c
0c |
159 | 158 | a1i 10 |
. . . . . . . . . . . . 13
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![m](_m.gif) ![m](_m.gif) 1c 0c![)](rp.gif) |
160 | | addcass 4415 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![m](_m.gif) 1c ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
161 | 160 | addceq1i 4386 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![m](_m.gif)
1c
![m](_m.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![m](_m.gif) ![)](rp.gif) |
162 | | addc32 4416 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![m](_m.gif)
1c
![m](_m.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![m](_m.gif) ![m](_m.gif) 1c![)](rp.gif) |
163 | 161, 162 | eqtr3i 2375 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![m](_m.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![m](_m.gif) ![m](_m.gif) 1c![)](rp.gif) |
164 | 163 | eqeq1i 2360 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![m](_m.gif)
0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![m](_m.gif) ![m](_m.gif) 1c 0c![)](rp.gif) |
165 | 159, 164 | sylnibr 296 |
. . . . . . . . . . . 12
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![m](_m.gif)
0c![)](rp.gif) |
166 | | peano2 4403 |
. . . . . . . . . . . . . . 15
![(](lp.gif) Nn ![(](lp.gif)
1c
Nn ![)](rp.gif) |
167 | | nncaddccl 4419 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
Nn ![(](lp.gif) 1c Nn ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) Nn ![)](rp.gif) |
168 | 167 | anidms 626 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif)
1c
Nn ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif)
Nn ![)](rp.gif) |
169 | 166, 168 | syl 15 |
. . . . . . . . . . . . . 14
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) Nn ![)](rp.gif) |
170 | | nncaddccl 4419 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) Nn Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![m](_m.gif)
Nn ![)](rp.gif) |
171 | 169, 170 | mpancom 650 |
. . . . . . . . . . . . 13
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![m](_m.gif) Nn ![)](rp.gif) |
172 | | peano1 4402 |
. . . . . . . . . . . . 13
0c
Nn |
173 | | suc11nnc 4558 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![m](_m.gif) Nn 0c
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![m](_m.gif) 1c 0c 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![m](_m.gif) 0c![)](rp.gif) ![)](rp.gif) |
174 | 171, 172,
173 | sylancl 643 |
. . . . . . . . . . . 12
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![m](_m.gif) 1c 0c
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![m](_m.gif)
0c![)](rp.gif) ![)](rp.gif) |
175 | 165, 174 | mtbird 292 |
. . . . . . . . . . 11
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![m](_m.gif) 1c 0c
1c![)](rp.gif) ![)](rp.gif) |
176 | | addcass 4415 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![m](_m.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
177 | 176 | eqeq1i 2360 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![m](_m.gif) 1c 0c 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif)
0c
1c![)](rp.gif) ![)](rp.gif) |
178 | 175, 177 | sylnib 295 |
. . . . . . . . . 10
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) 0c 1c![)](rp.gif) ![)](rp.gif) |
179 | | addceq12 4385 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif)
0c 0c ![(](lp.gif)
![p](_p.gif)
0c
0c![)](rp.gif) ![)](rp.gif) |
180 | 179 | anidms 626 |
. . . . . . . . . . . . . . 15
![(](lp.gif) 0c ![(](lp.gif) ![p](_p.gif)
0c
0c![)](rp.gif) ![)](rp.gif) |
181 | | id 19 |
. . . . . . . . . . . . . . 15
![(](lp.gif) 0c
0c![)](rp.gif) |
182 | 180, 181 | addceq12d 4391 |
. . . . . . . . . . . . . 14
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![p](_p.gif)
![(](lp.gif) 0c 0c 0c![)](rp.gif) ![)](rp.gif) |
183 | 182, 103 | syl6eq 2401 |
. . . . . . . . . . . . 13
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![p](_p.gif)
0c![)](rp.gif) |
184 | 183 | addceq1d 4389 |
. . . . . . . . . . . 12
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif) ![p](_p.gif) 1c 0c
1c![)](rp.gif) ![)](rp.gif) |
185 | 184 | eqeq2d 2364 |
. . . . . . . . . . 11
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![p](_p.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) 0c 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
186 | 185 | notbid 285 |
. . . . . . . . . 10
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![p](_p.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) 0c 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
187 | 178, 186 | syl5ibrcom 213 |
. . . . . . . . 9
![(](lp.gif) Nn ![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![p](_p.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
188 | 187 | adantr 451 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif)
![m](_m.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![(](lp.gif)
0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![p](_p.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
189 | | addceq12 4385 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif)
![q](_q.gif) ![(](lp.gif) ![n](_n.gif)
![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) |
190 | 189 | anidms 626 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) |
191 | | id 19 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![q](_q.gif) ![)](rp.gif) |
192 | 190, 191 | addceq12d 4391 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![)](rp.gif) ![)](rp.gif) |
193 | 192 | addceq1d 4389 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) ![q](_q.gif) 1c![)](rp.gif) ![)](rp.gif) |
194 | 193 | eqeq2d 2364 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) ![m](_m.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![q](_q.gif) ![q](_q.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
195 | 194 | notbid 285 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
![m](_m.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
![m](_m.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![q](_q.gif) ![q](_q.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
196 | 195 | rspcv 2951 |
. . . . . . . . . . . . . 14
![(](lp.gif) Nn ![(](lp.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif)
![m](_m.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif)
![m](_m.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) ![q](_q.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
197 | 196 | adantl 452 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
![m](_m.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) ![m](_m.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![q](_q.gif) ![q](_q.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
198 | | addc6 4418 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
![m](_m.gif) ![(](lp.gif) 1c
1c
1c![)](rp.gif) ![)](rp.gif) |
199 | | addc6 4418 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif) 1c
1c
1c![)](rp.gif) ![)](rp.gif) |
200 | 199 | addceq1i 4386 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif) 1c
1c
1c![)](rp.gif)
1c![)](rp.gif) |
201 | | addc32 4416 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif) 1c
1c
1c![)](rp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) 1c ![(](lp.gif) 1c 1c 1c![)](rp.gif) ![)](rp.gif) |
202 | 200, 201 | eqtri 2373 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) 1c ![(](lp.gif) 1c 1c 1c![)](rp.gif) ![)](rp.gif) |
203 | 198, 202 | eqeq12i 2366 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) ![m](_m.gif) ![(](lp.gif) 1c 1c 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) ![q](_q.gif) 1c ![(](lp.gif) 1c 1c 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
204 | | nncaddccl 4419 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![m](_m.gif) Nn ![)](rp.gif) |
205 | 204 | anidms 626 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) Nn ![(](lp.gif) ![m](_m.gif)
Nn ![)](rp.gif) |
206 | | nncaddccl 4419 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
Nn
Nn ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) ![m](_m.gif) Nn ![)](rp.gif) |
207 | 205, 206 | mpancom 650 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
![m](_m.gif)
Nn ![)](rp.gif) |
208 | | nncaddccl 4419 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![q](_q.gif) Nn ![)](rp.gif) |
209 | 208 | anidms 626 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) Nn ![(](lp.gif) ![q](_q.gif)
Nn ![)](rp.gif) |
210 | | nncaddccl 4419 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
Nn
Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) ![q](_q.gif) Nn ![)](rp.gif) |
211 | 209, 210 | mpancom 650 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif)
Nn ![)](rp.gif) |
212 | | peano2 4403 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) ![q](_q.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) ![q](_q.gif) 1c Nn ![)](rp.gif) |
213 | 211, 212 | syl 15 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) ![q](_q.gif) 1c Nn ![)](rp.gif) |
214 | | 1cnnc 4408 |
. . . . . . . . . . . . . . . . . . 19
1c
Nn |
215 | | nncaddccl 4419 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) 1c Nn 1c
Nn 1c
1c
Nn ![)](rp.gif) |
216 | 214, 214,
215 | mp2an 653 |
. . . . . . . . . . . . . . . . . 18
1c
1c
Nn |
217 | | nncaddccl 4419 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) 1c 1c
Nn 1c Nn ![(](lp.gif) 1c 1c 1c Nn ![)](rp.gif) |
218 | 216, 214,
217 | mp2an 653 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) 1c 1c 1c
Nn |
219 | | addccan1 4560 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
![m](_m.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) ![q](_q.gif) 1c Nn ![(](lp.gif) 1c
1c
1c
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
![m](_m.gif) ![(](lp.gif) 1c
1c
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) ![q](_q.gif) 1c ![(](lp.gif) 1c 1c 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![m](_m.gif) ![m](_m.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) ![q](_q.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
220 | 218, 219 | mp3an3 1266 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
![m](_m.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) ![q](_q.gif) 1c Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
![m](_m.gif) ![(](lp.gif) 1c
1c
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) ![q](_q.gif) 1c ![(](lp.gif) 1c 1c 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![m](_m.gif) ![m](_m.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) ![q](_q.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
221 | 207, 213,
220 | syl2an 463 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
![m](_m.gif) ![(](lp.gif) 1c
1c
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) ![q](_q.gif) 1c ![(](lp.gif) 1c 1c 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![m](_m.gif) ![m](_m.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) ![q](_q.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
222 | 203, 221 | syl5bb 248 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) ![m](_m.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![q](_q.gif) ![q](_q.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
223 | 222 | biimpd 198 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
224 | 197, 223 | nsyld 132 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![m](_m.gif)
![m](_m.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
225 | 224 | imp 418 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![m](_m.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) |
226 | 225 | an32s 779 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif)
![m](_m.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) |
227 | | addceq12 4385 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![p](_p.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
228 | 227 | anidms 626 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![p](_p.gif)
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
229 | | id 19 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
230 | 228, 229 | addceq12d 4391 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![p](_p.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
231 | 230 | addceq1d 4389 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif) ![p](_p.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif)
1c![)](rp.gif) ![)](rp.gif) |
232 | 231 | eqeq2d 2364 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![p](_p.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
233 | 232 | notbid 285 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![p](_p.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
234 | 226, 233 | syl5ibrcom 213 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif)
![m](_m.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) Nn ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![p](_p.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
235 | 234 | rexlimdva 2738 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif)
![m](_m.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![p](_p.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
236 | 188, 235 | jaod 369 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif)
![m](_m.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
0c
![E.](exists.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![p](_p.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
237 | 155, 236 | syl5bi 208 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif)
![m](_m.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![p](_p.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
238 | 237 | ralrimiv 2696 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif)
![m](_m.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![p](_p.gif) ![p](_p.gif) 1c![)](rp.gif) ![)](rp.gif) |
239 | 238 | ex 423 |
. . . 4
![(](lp.gif) Nn ![(](lp.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif)
![m](_m.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![p](_p.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
240 | 96, 107, 114, 130, 137, 154, 239 | finds 4411 |
. . 3
![(](lp.gif) Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![A](_ca.gif) ![A](_ca.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
241 | | addceq12 4385 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif)
![B](_cb.gif) ![(](lp.gif) ![n](_n.gif)
![(](lp.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
242 | 241 | anidms 626 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![(](lp.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
243 | | id 19 |
. . . . . . . 8
![(](lp.gif) ![B](_cb.gif) ![)](rp.gif) |
244 | 242, 243 | addceq12d 4391 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![B](_cb.gif)
![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
245 | 244 | addceq1d 4389 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![B](_cb.gif) ![B](_cb.gif) 1c![)](rp.gif) ![)](rp.gif) |
246 | 245 | eqeq2d 2364 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A](_ca.gif) ![A](_ca.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![A](_ca.gif) ![A](_ca.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![B](_cb.gif) ![B](_cb.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
247 | 246 | notbid 285 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A](_ca.gif)
![A](_ca.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![A](_ca.gif)
![A](_ca.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![B](_cb.gif) ![B](_cb.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
248 | 247 | rspccv 2952 |
. . 3
![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![A](_ca.gif)
![A](_ca.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![A](_ca.gif) ![A](_ca.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![B](_cb.gif)
![B](_cb.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
249 | 240, 248 | syl 15 |
. 2
![(](lp.gif) Nn ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![A](_ca.gif) ![A](_ca.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![B](_cb.gif)
![B](_cb.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
250 | 249 | imp 418 |
1
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![(](lp.gif)
![A](_ca.gif) ![A](_ca.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![B](_cb.gif) ![B](_cb.gif) 1c![)](rp.gif) ![)](rp.gif) |