Step | Hyp | Ref
| Expression |
1 | | isof1o 5716 |
. . . . . . . . . . 11
![( (](lp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![H H](_ch.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![B B](_cb.gif) ![)
)](rp.gif) |
2 | | f1of 5375 |
. . . . . . . . . . 11
![( (](lp.gif) ![H H](_ch.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![H H](_ch.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-->
-->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) |
3 | | ffvelrn 5561 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif)
![A A](_ca.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![B B](_cb.gif) ![) )](rp.gif) |
4 | 3 | ex 114 |
. . . . . . . . . . . 12
![( (](lp.gif) ![H H](_ch.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![(
(](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
5 | | ffvelrn 5561 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif)
![A A](_ca.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![B B](_cb.gif) ![) )](rp.gif) |
6 | 5 | ex 114 |
. . . . . . . . . . . 12
![( (](lp.gif) ![H H](_ch.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![(
(](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
7 | | ffvelrn 5561 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif)
![A A](_ca.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![f f](_f.gif) ![B B](_cb.gif) ![) )](rp.gif) |
8 | 7 | ex 114 |
. . . . . . . . . . . 12
![( (](lp.gif) ![H H](_ch.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![(
(](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![f f](_f.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
9 | 4, 6, 8 | 3anim123d 1298 |
. . . . . . . . . . 11
![( (](lp.gif) ![H H](_ch.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![(
(](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![(
(](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![( (](lp.gif) ![H H](_ch.gif) ![`
`](backtick.gif) ![f f](_f.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
10 | 1, 2, 9 | 3syl 17 |
. . . . . . . . . 10
![( (](lp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![(
(](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![( (](lp.gif) ![H H](_ch.gif) ![`
`](backtick.gif) ![f f](_f.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
11 | 10 | imp 123 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif)
![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![`
`](backtick.gif) ![d d](_d.gif)
![( (](lp.gif) ![H H](_ch.gif) ![`
`](backtick.gif) ![e e](_e.gif)
![( (](lp.gif) ![H H](_ch.gif) ![`
`](backtick.gif) ![f f](_f.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
12 | | breq12 3942 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![(
(](lp.gif) ![a a](_a.gif) ![S S](_cs.gif) ![(
(](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![)
)](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
13 | 12 | anidms 395 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![( (](lp.gif) ![a
a](_a.gif) ![S S](_cs.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
14 | 13 | notbid 657 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![( (](lp.gif) ![a a](_a.gif) ![S S](_cs.gif)
![( (](lp.gif) ![H H](_ch.gif) ![`
`](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
15 | | breq1 3940 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![( (](lp.gif) ![a
a](_a.gif) ![S S](_cs.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![b b](_b.gif) ![) )](rp.gif) ![) )](rp.gif) |
16 | 15 | anbi1d 461 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![( (](lp.gif) ![(
(](lp.gif) ![a a](_a.gif) ![S S](_cs.gif) ![b b](_b.gif) ![S S](_cs.gif) ![c c](_c.gif) ![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![b b](_b.gif) ![S S](_cs.gif) ![c c](_c.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
17 | | breq1 3940 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![( (](lp.gif) ![a
a](_a.gif) ![S S](_cs.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![c c](_c.gif) ![) )](rp.gif) ![) )](rp.gif) |
18 | 16, 17 | imbi12d 233 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![a a](_a.gif) ![S S](_cs.gif) ![b b](_b.gif) ![S S](_cs.gif) ![c c](_c.gif) ![a a](_a.gif) ![S S](_cs.gif) ![c c](_c.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![)
)](rp.gif) ![S S](_cs.gif) ![b b](_b.gif) ![S S](_cs.gif) ![c c](_c.gif) ![(
(](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![)
)](rp.gif) ![S S](_cs.gif) ![c c](_c.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
19 | 14, 18 | anbi12d 465 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![( (](lp.gif) ![(
(](lp.gif) ![a a](_a.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![a a](_a.gif) ![S S](_cs.gif) ![b b](_b.gif) ![S S](_cs.gif) ![c c](_c.gif) ![a
a](_a.gif) ![S S](_cs.gif) ![c c](_c.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![`
`](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![b b](_b.gif) ![S S](_cs.gif) ![c c](_c.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![c c](_c.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
20 | | breq2 3941 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![( (](lp.gif) ![(
(](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![)
)](rp.gif) ![S S](_cs.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
21 | | breq1 3940 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![( (](lp.gif) ![b
b](_b.gif) ![S S](_cs.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![) )](rp.gif) ![S S](_cs.gif) ![c c](_c.gif) ![) )](rp.gif) ![) )](rp.gif) |
22 | 20, 21 | anbi12d 465 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![b b](_b.gif) ![S S](_cs.gif) ![c c](_c.gif) ![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![) )](rp.gif) ![S S](_cs.gif) ![c c](_c.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
23 | 22 | imbi1d 230 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![b b](_b.gif) ![S S](_cs.gif) ![c c](_c.gif) ![( (](lp.gif) ![H H](_ch.gif) ![`
`](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![c c](_c.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![)
)](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![) )](rp.gif) ![S S](_cs.gif) ![c c](_c.gif) ![(
(](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![)
)](rp.gif) ![S S](_cs.gif) ![c c](_c.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
24 | 23 | anbi2d 460 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![)
)](rp.gif) ![S S](_cs.gif) ![b b](_b.gif) ![S S](_cs.gif) ![c c](_c.gif) ![(
(](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![)
)](rp.gif) ![S S](_cs.gif) ![c c](_c.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![`
`](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![) )](rp.gif) ![S S](_cs.gif) ![c c](_c.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![c c](_c.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
25 | | breq2 3941 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![f f](_f.gif) ![( (](lp.gif) ![(
(](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![)
)](rp.gif) ![S S](_cs.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
26 | 25 | anbi2d 460 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![f f](_f.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![) )](rp.gif) ![S S](_cs.gif) ![c c](_c.gif) ![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
27 | | breq2 3941 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![f f](_f.gif) ![( (](lp.gif) ![(
(](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![)
)](rp.gif) ![S S](_cs.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
28 | 26, 27 | imbi12d 233 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![f f](_f.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![) )](rp.gif) ![S S](_cs.gif) ![c c](_c.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![c c](_c.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![( (](lp.gif) ![H H](_ch.gif) ![`
`](backtick.gif) ![e e](_e.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![(
(](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![)
)](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
29 | 28 | anbi2d 460 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![f f](_f.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![)
)](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![) )](rp.gif) ![S S](_cs.gif) ![c c](_c.gif) ![(
(](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![)
)](rp.gif) ![S S](_cs.gif) ![c c](_c.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![`
`](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
30 | 19, 24, 29 | rspc3v 2809 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![( (](lp.gif) ![H H](_ch.gif) ![`
`](backtick.gif) ![f f](_f.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![A. A.](forall.gif)
![A. A.](forall.gif)
![( (](lp.gif)
![a a](_a.gif) ![S S](_cs.gif)
![( (](lp.gif) ![( (](lp.gif) ![a
a](_a.gif) ![S S](_cs.gif) ![b b](_b.gif) ![S S](_cs.gif) ![c c](_c.gif) ![a
a](_a.gif) ![S S](_cs.gif) ![c c](_c.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
31 | 11, 30 | syl 14 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif)
![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![A. A.](forall.gif)
![A. A.](forall.gif)
![A. A.](forall.gif)
![( (](lp.gif) ![a a](_a.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![a a](_a.gif) ![S S](_cs.gif) ![b b](_b.gif) ![S S](_cs.gif) ![c c](_c.gif) ![a a](_a.gif) ![S S](_cs.gif) ![c c](_c.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![`
`](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
32 | | simpl 108 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif)
![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif)
![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
33 | | simpr1 988 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif)
![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif)
![A A](_ca.gif) ![) )](rp.gif) |
34 | | isorel 5717 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif)
![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![d d](_d.gif) ![R R](_cr.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
35 | 32, 33, 33, 34 | syl12anc 1215 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif)
![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![d d](_d.gif) ![R R](_cr.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
36 | 35 | notbid 657 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif)
![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![d d](_d.gif) ![R R](_cr.gif)
![( (](lp.gif) ![H H](_ch.gif) ![`
`](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
37 | | simpr2 989 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif)
![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif)
![A A](_ca.gif) ![) )](rp.gif) |
38 | | isorel 5717 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif)
![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![d d](_d.gif) ![R R](_cr.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
39 | 32, 33, 37, 38 | syl12anc 1215 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif)
![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![d d](_d.gif) ![R R](_cr.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
40 | | simpr3 990 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif)
![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif)
![A A](_ca.gif) ![) )](rp.gif) |
41 | | isorel 5717 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif)
![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![e e](_e.gif) ![R R](_cr.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
42 | 32, 37, 40, 41 | syl12anc 1215 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif)
![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![e e](_e.gif) ![R R](_cr.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
43 | 39, 42 | anbi12d 465 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif)
![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![d
d](_d.gif) ![R R](_cr.gif) ![e e](_e.gif) ![R R](_cr.gif) ![f f](_f.gif)
![( (](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![`
`](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![( (](lp.gif) ![H H](_ch.gif) ![`
`](backtick.gif) ![e e](_e.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
44 | | isorel 5717 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif)
![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![d d](_d.gif) ![R R](_cr.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
45 | 32, 33, 40, 44 | syl12anc 1215 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif)
![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![d d](_d.gif) ![R R](_cr.gif)
![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
46 | 43, 45 | imbi12d 233 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif)
![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![d d](_d.gif) ![R R](_cr.gif) ![e e](_e.gif) ![R R](_cr.gif) ![f f](_f.gif)
![d d](_d.gif) ![R R](_cr.gif) ![f
f](_f.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![)
)](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![(
(](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![)
)](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
47 | 36, 46 | anbi12d 465 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif)
![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![d d](_d.gif) ![R R](_cr.gif) ![( (](lp.gif) ![( (](lp.gif) ![d d](_d.gif) ![R R](_cr.gif) ![e e](_e.gif) ![R R](_cr.gif) ![f f](_f.gif) ![d d](_d.gif) ![R R](_cr.gif) ![f f](_f.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![)
)](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![e e](_e.gif) ![) )](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![(
(](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![d d](_d.gif) ![)
)](rp.gif) ![S S](_cs.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
48 | 31, 47 | sylibrd 168 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif)
![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![A. A.](forall.gif)
![A. A.](forall.gif)
![A. A.](forall.gif)
![( (](lp.gif) ![a a](_a.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![a a](_a.gif) ![S S](_cs.gif) ![b b](_b.gif) ![S S](_cs.gif) ![c c](_c.gif) ![a a](_a.gif) ![S S](_cs.gif) ![c c](_c.gif) ![) )](rp.gif) ![( (](lp.gif) ![d d](_d.gif) ![R R](_cr.gif) ![( (](lp.gif) ![(
(](lp.gif) ![d d](_d.gif) ![R R](_cr.gif) ![e e](_e.gif) ![R R](_cr.gif) ![f f](_f.gif)
![d d](_d.gif) ![R R](_cr.gif) ![f
f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
49 | 48 | ex 114 |
. . . . . 6
![( (](lp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![A. A.](forall.gif)
![A. A.](forall.gif)
![( (](lp.gif)
![a a](_a.gif) ![S S](_cs.gif)
![( (](lp.gif) ![( (](lp.gif) ![a
a](_a.gif) ![S S](_cs.gif) ![b b](_b.gif) ![S S](_cs.gif) ![c c](_c.gif) ![a
a](_a.gif) ![S S](_cs.gif) ![c c](_c.gif) ![) )](rp.gif)
![( (](lp.gif) ![d d](_d.gif) ![R R](_cr.gif) ![( (](lp.gif) ![(
(](lp.gif) ![d d](_d.gif) ![R R](_cr.gif) ![e e](_e.gif) ![R R](_cr.gif) ![f f](_f.gif)
![d d](_d.gif) ![R R](_cr.gif) ![f
f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
50 | 49 | com23 78 |
. . . . 5
![( (](lp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![A. A.](forall.gif)
![A. A.](forall.gif)
![( (](lp.gif) ![a a](_a.gif) ![S S](_cs.gif) ![( (](lp.gif) ![(
(](lp.gif) ![a a](_a.gif) ![S S](_cs.gif) ![b b](_b.gif) ![S S](_cs.gif) ![c c](_c.gif)
![a a](_a.gif) ![S S](_cs.gif) ![c
c](_c.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![d d](_d.gif) ![R R](_cr.gif) ![( (](lp.gif) ![( (](lp.gif) ![d d](_d.gif) ![R R](_cr.gif) ![e e](_e.gif) ![R R](_cr.gif) ![f f](_f.gif) ![d d](_d.gif) ![R R](_cr.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
51 | 50 | imp31 254 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R R](_cr.gif)
![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![A. A.](forall.gif)
![A. A.](forall.gif)
![A. A.](forall.gif)
![( (](lp.gif) ![a a](_a.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![a a](_a.gif) ![S S](_cs.gif) ![b b](_b.gif) ![S S](_cs.gif) ![c c](_c.gif) ![a a](_a.gif) ![S S](_cs.gif) ![c c](_c.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif) ![(
(](lp.gif) ![d d](_d.gif) ![R R](_cr.gif) ![( (](lp.gif) ![( (](lp.gif) ![d d](_d.gif) ![R R](_cr.gif) ![e e](_e.gif) ![R R](_cr.gif) ![f f](_f.gif) ![d
d](_d.gif) ![R R](_cr.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
52 | 51 | ralrimivvva 2518 |
. . 3
![( (](lp.gif) ![( (](lp.gif)
![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![A. A.](forall.gif)
![A. A.](forall.gif)
![A. A.](forall.gif)
![( (](lp.gif) ![a a](_a.gif) ![S S](_cs.gif) ![( (](lp.gif) ![( (](lp.gif) ![a a](_a.gif) ![S S](_cs.gif) ![b b](_b.gif) ![S S](_cs.gif) ![c c](_c.gif) ![a a](_a.gif) ![S S](_cs.gif) ![c c](_c.gif) ![) )](rp.gif) ![) )](rp.gif)
![A. A.](forall.gif)
![A. A.](forall.gif)
![A. A.](forall.gif)
![( (](lp.gif) ![d d](_d.gif) ![R R](_cr.gif) ![( (](lp.gif) ![(
(](lp.gif) ![d d](_d.gif) ![R R](_cr.gif) ![e e](_e.gif) ![R R](_cr.gif) ![f f](_f.gif)
![d d](_d.gif) ![R R](_cr.gif) ![f
f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
53 | 52 | ex 114 |
. 2
![( (](lp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![A. A.](forall.gif)
![A. A.](forall.gif)
![( (](lp.gif) ![a a](_a.gif) ![S S](_cs.gif) ![( (](lp.gif) ![(
(](lp.gif) ![a a](_a.gif) ![S S](_cs.gif) ![b b](_b.gif) ![S S](_cs.gif) ![c c](_c.gif)
![a a](_a.gif) ![S S](_cs.gif) ![c
c](_c.gif) ![) )](rp.gif) ![A. A.](forall.gif)
![A. A.](forall.gif)
![A. A.](forall.gif)
![( (](lp.gif)
![d d](_d.gif) ![R R](_cr.gif)
![( (](lp.gif) ![( (](lp.gif) ![d
d](_d.gif) ![R R](_cr.gif) ![e e](_e.gif) ![R R](_cr.gif) ![f f](_f.gif) ![d
d](_d.gif) ![R R](_cr.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
54 | | df-po 4226 |
. 2
![( (](lp.gif)
![A. A.](forall.gif)
![A. A.](forall.gif)
![A. A.](forall.gif)
![( (](lp.gif) ![a a](_a.gif) ![S S](_cs.gif) ![( (](lp.gif) ![(
(](lp.gif) ![a a](_a.gif) ![S S](_cs.gif) ![b b](_b.gif) ![S S](_cs.gif) ![c c](_c.gif)
![a a](_a.gif) ![S S](_cs.gif) ![c
c](_c.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
55 | | df-po 4226 |
. 2
![( (](lp.gif)
![A. A.](forall.gif)
![A. A.](forall.gif)
![A. A.](forall.gif)
![( (](lp.gif) ![d d](_d.gif) ![R R](_cr.gif) ![( (](lp.gif) ![(
(](lp.gif) ![d d](_d.gif) ![R R](_cr.gif) ![e e](_e.gif) ![R R](_cr.gif) ![f f](_f.gif)
![d d](_d.gif) ![R R](_cr.gif) ![f
f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
56 | 53, 54, 55 | 3imtr4g 204 |
1
![( (](lp.gif) ![R R](_cr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) |