![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 4t3lem | Unicode version |
Description: Lemma for 4t3e12 9035 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.) |
Ref | Expression |
---|---|
4t3lem.1 |
![]() ![]() ![]() ![]() |
4t3lem.2 |
![]() ![]() ![]() ![]() |
4t3lem.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4t3lem.4 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4t3lem.5 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
4t3lem |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 4t3lem.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | oveq2i 5677 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 4t3lem.1 |
. . . . . 6
![]() ![]() ![]() ![]() | |
4 | 3 | nn0cni 8746 |
. . . . 5
![]() ![]() ![]() ![]() |
5 | 4t3lem.2 |
. . . . . 6
![]() ![]() ![]() ![]() | |
6 | 5 | nn0cni 8746 |
. . . . 5
![]() ![]() ![]() ![]() |
7 | ax-1cn 7499 |
. . . . 5
![]() ![]() ![]() ![]() | |
8 | 4, 6, 7 | adddii 7559 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 4t3lem.4 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
10 | 4 | mulid1i 7551 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 9, 10 | oveq12i 5678 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 8, 11 | eqtri 2109 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 4t3lem.5 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
14 | 12, 13 | eqtri 2109 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 2, 14 | eqtri 2109 |
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 105 ax-ia2 106 ax-ia3 107 ax-io 666 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-10 1442 ax-11 1443 ax-i12 1444 ax-bndl 1445 ax-4 1446 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 ax-sep 3963 ax-cnex 7497 ax-resscn 7498 ax-1cn 7499 ax-1re 7500 ax-icn 7501 ax-addcl 7502 ax-addrcl 7503 ax-mulcl 7504 ax-mulcom 7507 ax-mulass 7509 ax-distr 7510 ax-1rid 7513 ax-rnegex 7515 ax-cnre 7517 |
This theorem depends on definitions: df-bi 116 df-3an 927 df-tru 1293 df-nf 1396 df-sb 1694 df-clab 2076 df-cleq 2082 df-clel 2085 df-nfc 2218 df-ral 2365 df-rex 2366 df-v 2622 df-un 3004 df-in 3006 df-ss 3013 df-sn 3456 df-pr 3457 df-op 3459 df-uni 3660 df-int 3695 df-br 3852 df-iota 4993 df-fv 5036 df-ov 5669 df-inn 8484 df-n0 8735 |
This theorem is referenced by: 4t3e12 9035 4t4e16 9036 5t2e10 9037 5t3e15 9038 5t4e20 9039 5t5e25 9040 6t3e18 9042 6t4e24 9043 6t5e30 9044 6t6e36 9045 7t3e21 9047 7t4e28 9048 7t5e35 9049 7t6e42 9050 7t7e49 9051 8t3e24 9053 8t4e32 9054 8t5e40 9055 8t6e48 9056 8t7e56 9057 8t8e64 9058 9t3e27 9060 9t4e36 9061 9t5e45 9062 9t6e54 9063 9t7e63 9064 9t8e72 9065 9t9e81 9066 |
Copyright terms: Public domain | W3C validator |