Step | Hyp | Ref
| Expression |
1 | | updjud.f |
. . . . 5
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![C C](_cc.gif) ![) )](rp.gif) |
2 | | updjud.g |
. . . . 5
![( (](lp.gif) ![G G](_cg.gif) ![: :](colon.gif) ![B B](_cb.gif) ![--> -->](longrightarrow.gif) ![C C](_cc.gif) ![) )](rp.gif) |
3 | | updjudhf.h |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ⊔ ![B B](_cb.gif) ![if if](_if.gif) ![( (](lp.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
4 | 1, 2, 3 | updjudhf 6972 |
. . . 4
![( (](lp.gif) ![H H](_ch.gif) ![: :](colon.gif) ![( (](lp.gif) ⊔ ![B B](_cb.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![C C](_cc.gif) ![) )](rp.gif) |
5 | | ffn 5280 |
. . . 4
![( (](lp.gif) ![H H](_ch.gif) ![: :](colon.gif) ![( (](lp.gif) ⊔ ![B B](_cb.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif)
![( (](lp.gif)
⊔ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
6 | 4, 5 | syl 14 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ⊔ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
7 | | inrresf1 6955 |
. . . 4
inr ![B B](_cb.gif) ![) )](rp.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-1-1-> -1-1->](onetoone.gif) ![( (](lp.gif) ⊔ ![B B](_cb.gif) ![) )](rp.gif) |
8 | | f1fn 5338 |
. . . 4
![( (](lp.gif) inr ![B B](_cb.gif) ![) )](rp.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-1-1-> -1-1->](onetoone.gif) ![( (](lp.gif) ⊔ ![B B](_cb.gif) inr ![B B](_cb.gif) ![B B](_cb.gif) ![)
)](rp.gif) |
9 | 7, 8 | mp1i 10 |
. . 3
![( (](lp.gif) inr ![B B](_cb.gif) ![B B](_cb.gif) ![) )](rp.gif) |
10 | | f1f 5336 |
. . . . 5
![( (](lp.gif) inr ![B B](_cb.gif) ![) )](rp.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-1-1-> -1-1->](onetoone.gif) ![( (](lp.gif) ⊔ ![B B](_cb.gif) inr ![B B](_cb.gif) ![) )](rp.gif) ![: :](colon.gif) ![B B](_cb.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif)
⊔ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
11 | 7, 10 | ax-mp 5 |
. . . 4
inr ![B B](_cb.gif) ![) )](rp.gif) ![: :](colon.gif) ![B B](_cb.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif) ⊔ ![B B](_cb.gif) ![) )](rp.gif) |
12 | | frn 5289 |
. . . 4
![( (](lp.gif) inr ![B B](_cb.gif) ![) )](rp.gif) ![: :](colon.gif) ![B B](_cb.gif) ![--> -->](longrightarrow.gif) ![( (](lp.gif)
⊔ ![B B](_cb.gif) inr ![B B](_cb.gif) ![( (](lp.gif)
⊔ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
13 | 11, 12 | mp1i 10 |
. . 3
![( (](lp.gif) inr ![B B](_cb.gif) ![( (](lp.gif) ⊔ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
14 | | fnco 5239 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ⊔ ![B B](_cb.gif) inr ![B B](_cb.gif) inr ![B B](_cb.gif) ![( (](lp.gif) ⊔ ![B B](_cb.gif) ![) )](rp.gif)
![( (](lp.gif) inr ![B B](_cb.gif) ![) )](rp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
15 | 6, 9, 13, 14 | syl3anc 1217 |
. 2
![( (](lp.gif) ![( (](lp.gif) inr ![B B](_cb.gif) ![) )](rp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
16 | | ffn 5280 |
. . 3
![( (](lp.gif) ![G G](_cg.gif) ![: :](colon.gif) ![B B](_cb.gif) ![--> -->](longrightarrow.gif)
![B B](_cb.gif) ![) )](rp.gif) |
17 | 2, 16 | syl 14 |
. 2
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
18 | | fvco2 5498 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) inr ![B B](_cb.gif) ![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif) inr ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![b b](_b.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![( (](lp.gif) inr ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![b b](_b.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
19 | 9, 18 | sylan 281 |
. . 3
![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif) inr ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![b b](_b.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) ![( (](lp.gif) inr ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![b b](_b.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
20 | | fvres 5453 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) inr ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![b b](_b.gif) inr![`
`](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![) )](rp.gif) |
21 | 20 | adantl 275 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![( (](lp.gif) inr ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![b b](_b.gif) inr![`
`](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![) )](rp.gif) |
22 | 21 | fveq2d 5433 |
. . . 4
![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![( (](lp.gif) ![H H](_ch.gif) ![`
`](backtick.gif) ![( (](lp.gif) inr ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![b b](_b.gif) ![)
)](rp.gif) ![( (](lp.gif) ![H H](_ch.gif) ![` `](backtick.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
23 | 3 | a1i 9 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ⊔
![B B](_cb.gif) ![if if](_if.gif) ![( (](lp.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
24 | | fveq2 5429 |
. . . . . . . . 9
![( (](lp.gif) inr![` `](backtick.gif) ![b b](_b.gif)
![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
25 | 24 | eqeq1d 2149 |
. . . . . . . 8
![( (](lp.gif) inr![` `](backtick.gif) ![b b](_b.gif)
![( (](lp.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) |
26 | | fveq2 5429 |
. . . . . . . . 9
![( (](lp.gif) inr![` `](backtick.gif) ![b b](_b.gif)
![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
27 | 26 | fveq2d 5433 |
. . . . . . . 8
![( (](lp.gif) inr![` `](backtick.gif) ![b b](_b.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![x x](_x.gif) ![)
)](rp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) inr![`
`](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
28 | 26 | fveq2d 5433 |
. . . . . . . 8
![( (](lp.gif) inr![` `](backtick.gif) ![b b](_b.gif)
![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![x x](_x.gif) ![)
)](rp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) inr![`
`](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
29 | 25, 27, 28 | ifbieq12d 3503 |
. . . . . . 7
![( (](lp.gif) inr![` `](backtick.gif) ![b b](_b.gif)
![if if](_if.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![if if](_if.gif) ![( (](lp.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![(/) (/)](varnothing.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
30 | 29 | adantl 275 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) inr![`
`](backtick.gif) ![b b](_b.gif) ![) )](rp.gif)
![if if](_if.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![if if](_if.gif) ![( (](lp.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![(/) (/)](varnothing.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
31 | | 1stinr 6969 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![)
)](rp.gif) ![1o 1o](_1o.gif) ![) )](rp.gif) |
32 | | 1n0 6337 |
. . . . . . . . . . . 12
![(/) (/)](varnothing.gif) |
33 | 32 | neii 2311 |
. . . . . . . . . . 11
![(/) (/)](varnothing.gif) |
34 | | eqeq1 2147 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![)
)](rp.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) ![) )](rp.gif) |
35 | 33, 34 | mtbiri 665 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![) )](rp.gif)
![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![)
)](rp.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) |
36 | 31, 35 | syl 14 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) |
37 | 36 | adantl 275 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) |
38 | 37 | adantr 274 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) inr![`
`](backtick.gif) ![b b](_b.gif) ![) )](rp.gif)
![( (](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![)
)](rp.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) |
39 | 38 | iffalsed 3489 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) inr![`
`](backtick.gif) ![b b](_b.gif) ![) )](rp.gif)
![if if](_if.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![(/) (/)](varnothing.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
40 | 30, 39 | eqtrd 2173 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) inr![`
`](backtick.gif) ![b b](_b.gif) ![) )](rp.gif)
![if if](_if.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1st 1st](_1st.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(/) (/)](varnothing.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
41 | | djurcl 6945 |
. . . . . 6
![( (](lp.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![( (](lp.gif) ⊔ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
42 | 41 | adantl 275 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![( (](lp.gif) ⊔ ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
43 | 2 | adantr 274 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![G G](_cg.gif) ![: :](colon.gif) ![B B](_cb.gif) ![--> -->](longrightarrow.gif) ![C C](_cc.gif) ![) )](rp.gif) |
44 | | 2ndinr 6970 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![)
)](rp.gif) ![b b](_b.gif) ![) )](rp.gif) |
45 | 44 | adantl 275 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![)
)](rp.gif) ![b b](_b.gif) ![) )](rp.gif) |
46 | | simpr 109 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![B B](_cb.gif) ![) )](rp.gif) |
47 | 45, 46 | eqeltrd 2217 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![)
)](rp.gif) ![B B](_cb.gif) ![)
)](rp.gif) |
48 | 43, 47 | ffvelrnd 5564 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![( (](lp.gif) ![G G](_cg.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) inr![`
`](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![)
)](rp.gif) ![C C](_cc.gif) ![)
)](rp.gif) |
49 | 23, 40, 42, 48 | fvmptd 5510 |
. . . 4
![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![( (](lp.gif) ![H H](_ch.gif) ![`
`](backtick.gif) inr![` `](backtick.gif) ![b b](_b.gif) ![)
)](rp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) inr![`
`](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
50 | 22, 49 | eqtrd 2173 |
. . 3
![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![( (](lp.gif) ![H H](_ch.gif) ![`
`](backtick.gif) ![( (](lp.gif) inr ![B B](_cb.gif) ![) )](rp.gif) ![` `](backtick.gif) ![b b](_b.gif) ![)
)](rp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) inr![`
`](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
51 | 45 | fveq2d 5433 |
. . 3
![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![( (](lp.gif) ![G G](_cg.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![2nd 2nd](_2nd.gif) ![` `](backtick.gif) inr![`
`](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![) )](rp.gif) |
52 | 19, 50, 51 | 3eqtrd 2177 |
. 2
![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![( (](lp.gif) ![(
(](lp.gif) inr ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![` `](backtick.gif) ![b b](_b.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![b b](_b.gif) ![) )](rp.gif) ![) )](rp.gif) |
53 | 15, 17, 52 | eqfnfvd 5529 |
1
![( (](lp.gif) ![( (](lp.gif) inr ![B B](_cb.gif) ![) )](rp.gif) ![G G](_cg.gif) ![) )](rp.gif) |