![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > tfri1dALT | Unicode version |
Description: Alternate proof of tfri1d 6035 in terms of tfr1on 6050.
Although this does show that the tfr1on 6050 proof is general enough to
also prove tfri1d 6035, the tfri1d 6035 proof is simpler in places because it
does not need to deal with |
Ref | Expression |
---|---|
tfri1dALT.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
tfri1dALT.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
tfri1dALT |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tfrfun 6020 |
. . . 4
![]() ![]() ![]() ![]() ![]() | |
2 | tfri1dALT.1 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | funeqi 4992 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mpbir 144 |
. . 3
![]() ![]() ![]() |
5 | 4 | a1i 9 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | eqid 2085 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 6 | tfrlem8 6018 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() |
8 | 2 | dmeqi 4598 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | ordeq 4166 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
10 | 8, 9 | ax-mp 7 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 7, 10 | mpbir 144 |
. . . 4
![]() ![]() ![]() ![]() |
12 | ordsson 4275 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
13 | 11, 12 | mp1i 10 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | tfri1dALT.2 |
. . . . . . . . . 10
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
15 | simpl 107 |
. . . . . . . . . . 11
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
16 | 15 | alimi 1387 |
. . . . . . . . . 10
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | 14, 16 | syl 14 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
18 | 17 | 19.21bi 1493 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
19 | 18 | adantr 270 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
20 | ordon 4269 |
. . . . . . . 8
![]() ![]() ![]() | |
21 | 20 | a1i 9 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
22 | simpr 108 |
. . . . . . . . . . 11
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
23 | 22 | alimi 1387 |
. . . . . . . . . 10
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
24 | fveq2 5256 |
. . . . . . . . . . . 12
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
25 | 24 | eleq1d 2153 |
. . . . . . . . . . 11
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
26 | 25 | spv 1785 |
. . . . . . . . . 10
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
27 | 14, 23, 26 | 3syl 17 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
28 | 27 | adantr 270 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
29 | 28 | 3ad2ant1 962 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
30 | suceloni 4284 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
31 | unon 4294 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() | |
32 | 30, 31 | eleq2s 2179 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
33 | 32 | adantl 271 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
34 | suceloni 4284 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
35 | 34 | adantl 271 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
36 | 2, 19, 21, 29, 33, 35 | tfr1on 6050 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
37 | vex 2617 |
. . . . . . 7
![]() ![]() ![]() ![]() | |
38 | 37 | sucid 4211 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() |
39 | ssel2 3007 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
40 | 36, 38, 39 | sylancl 404 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
41 | 40 | ex 113 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
42 | 41 | ssrdv 3018 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
43 | 13, 42 | eqssd 3029 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
44 | df-fn 4975 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
45 | 5, 43, 44 | sylanbrc 408 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1379 ax-7 1380 ax-gen 1381 ax-ie1 1425 ax-ie2 1426 ax-8 1438 ax-10 1439 ax-11 1440 ax-i12 1441 ax-bndl 1442 ax-4 1443 ax-13 1447 ax-14 1448 ax-17 1462 ax-i9 1466 ax-ial 1470 ax-i5r 1471 ax-ext 2067 ax-coll 3922 ax-sep 3925 ax-pow 3977 ax-pr 4003 ax-un 4227 ax-setind 4319 |
This theorem depends on definitions: df-bi 115 df-3an 924 df-tru 1290 df-fal 1293 df-nf 1393 df-sb 1690 df-eu 1948 df-mo 1949 df-clab 2072 df-cleq 2078 df-clel 2081 df-nfc 2214 df-ne 2252 df-ral 2360 df-rex 2361 df-reu 2362 df-rab 2364 df-v 2616 df-sbc 2829 df-csb 2922 df-dif 2988 df-un 2990 df-in 2992 df-ss 2999 df-nul 3273 df-pw 3411 df-sn 3431 df-pr 3432 df-op 3434 df-uni 3631 df-iun 3709 df-br 3815 df-opab 3869 df-mpt 3870 df-tr 3905 df-id 4087 df-iord 4160 df-on 4162 df-suc 4165 df-xp 4410 df-rel 4411 df-cnv 4412 df-co 4413 df-dm 4414 df-rn 4415 df-res 4416 df-ima 4417 df-iota 4937 df-fun 4974 df-fn 4975 df-f 4976 df-f1 4977 df-fo 4978 df-f1o 4979 df-fv 4980 df-recs 6005 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |