Nearby theorems
|
|
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > ILE Home > Th. List > apcotr | Unicode version | ||
| Description: Apartness is cotransitive. (Contributed by Jim Kingdon, 16-Feb-2020.) |
| Ref | Expression |
|---|---|
| apcotr |
     ![/\](wedge.gif "/\"){kind=small} 
   #
#  # |
are mutually distinct and distinct from all other
variables.| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cnre 7474 |
. . 3
      | |
| 2 | 1 | 3ad2ant3 966 |
. 2
|
| 3 | cnre 7474 |
. . . . . . 7
| |
| 4 | 3 | 3ad2ant2 965 |
. . . . . 6
|
| 5 | 4 | ad2antrr 472 |
. . . . 5
|
| 6 | cnre 7474 |
. . . . . . . . . . 11
| |
| 7 | 6 | 3ad2ant1 964 |
. . . . . . . . . 10
|
| 8 | 7 | adantr 270 |
. . . . . . . . 9
|
| 9 | 8 | ad3antrrr 476 |
. . . . . . . 8
|
| 10 | simpr 108 |
. . . . . . . . . . . . . . 15
| |
| 11 | simpllr 501 |
. . . . . . . . . . . . . . 15
| |
| 12 | 10, 11 | breq12d 3856 |
. . . . . . . . . . . . . 14
#
# |
| 13 | simplrl 502 |
. . . . . . . . . . . . . . 15
| |
| 14 | simplrr 503 |
. . . . . . . . . . . . . . 15
| |
| 15 | simprl 498 |
. . . . . . . . . . . . . . . 16
| |
| 16 | 15 | ad3antrrr 476 |
. . . . . . . . . . . . . . 15
|
| 17 | simprr 499 |
. . . . . . . . . . . . . . . 16
| |
| 18 | 17 | ad3antrrr 476 |
. . . . . . . . . . . . . . 15
|
| 19 | apreim 8070 |
. . . . . . . . . . . . . . 15
#
#
# | |
| 20 | 13, 14, 16, 18, 19 | syl22anc 1175 |
. . . . . . . . . . . . . 14
#
#
# |
| 21 | 12, 20 | bitrd 186 |
. . . . . . . . . . . . 13
#
# # |
| 22 | simprl 498 |
. . . . . . . . . . . . . . . . 17
| |
| 23 | 22 | ad2antrr 472 |
. . . . . . . . . . . . . . . 16
|
| 24 | 23 | ad3antrrr 476 |
. . . . . . . . . . . . . . 15
|
| 25 | reapcotr 8065 |
. . . . . . . . . . . . . . 15
# # # | |
| 26 | 13, 16, 24, 25 | syl3anc 1174 |
. . . . . . . . . . . . . 14
# # # |
| 27 | simprr 499 |
. . . . . . . . . . . . . . . . 17
| |
| 28 | 27 | ad2antrr 472 |
. . . . . . . . . . . . . . . 16
|
| 29 | 28 | ad3antrrr 476 |
. . . . . . . . . . . . . . 15
|
| 30 | reapcotr 8065 |
. . . . . . . . . . . . . . 15
# # # | |
| 31 | 14, 18, 29, 30 | syl3anc 1174 |
. . . . . . . . . . . . . 14
# # # |
| 32 | 26, 31 | orim12d 735 |
. . . . . . . . . . . . 13
# # # #
# # |
| 33 | 21, 32 | sylbid 148 |
. . . . . . . . . . . 12
#
# # # # |
| 34 | or4 723 |
. . . . . . . . . . . 12
# # # # # #
# # | |
| 35 | 33, 34 | syl6ib 159 |
. . . . . . . . . . 11
#
# # # # |
| 36 | simplr 497 |
. . . . . . . . . . . . . . 15
| |
| 37 | 36 | ad3antrrr 476 |
. . . . . . . . . . . . . 14
|
| 38 | 10, 37 | breq12d 3856 |
. . . . . . . . . . . . 13
#
# |
| 39 | apreim 8070 |
. . . . . . . . . . . . . 14
#
#
# | |
| 40 | 13, 14, 24, 29, 39 | syl22anc 1175 |
. . . . . . . . . . . . 13
#
#
# |
| 41 | 38, 40 | bitrd 186 |
. . . . . . . . . . . 12
#
# #
|
| 42 | 11, 37 | breq12d 3856 |
. . . . . . . . . . . . 13
#
# |
| 43 | apreim 8070 |
. . . . . . . . . . . . . 14
#
#
# | |
| 44 | 16, 18, 24, 29, 43 | syl22anc 1175 |
. . . . . . . . . . . . 13
#
#
# |
| 45 | 42, 44 | bitrd 186 |
. . . . . . . . . . . 12
#
# # |
| 46 | 41, 45 | orbi12d 742 |
. . . . . . . . . . 11
# #
# # # # |
| 47 | 35, 46 | sylibrd 167 |
. . . . . . . . . 10
#
# # |
| 48 | 47 | ex 113 |
. . . . . . . . 9
#
# # |
| 49 | 48 | rexlimdvva 2496 |
. . . . . . . 8
#
# # |
| 50 | 9, 49 | mpd 13 |
. . . . . . 7
#
# # |
| 51 | 50 | ex 113 |
. . . . . 6
#
# # |
| 52 | 51 | rexlimdvva 2496 |
. . . . 5
#
# # |
| 53 | 5, 52 | mpd 13 |
. . . 4
#
# # |
| 54 | 53 | ex 113 |
. . 3
#
# # |
| 55 | 54 | rexlimdvva 2496 |
. 2
#
# # |
| 56 | 2, 55 | mpd 13 |
1
#
# # |
| Colors of variables: wff set class |
| Syntax hints: wi 4
wa 102
wb 103 wo 664 w3a 924 wceq 1289 wcel 1438 wrex 2360 class class class wbr 3843
(class class class)co 5644 cc 7338 cr 7339 ci 7342 caddc 7343 cmul 7345 # cap 8048 |
| 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 579 ax-in2 580 ax-io 665 ax-5 1381 ax-7 1382 ax-gen 1383 ax-ie1 1427 ax-ie2 1428 ax-8 1440 ax-10 1441 ax-11 1442 ax-i12 1443 ax-bndl 1444 ax-4 1445 ax-13 1449 ax-14 1450 ax-17 1464 ax-i9 1468 ax-ial 1472 ax-i5r 1473 ax-ext 2070 ax-sep 3955 ax-pow 4007 ax-pr 4034 ax-un 4258 ax-setind 4351 ax-cnex 7426 ax-resscn 7427 ax-1cn 7428 ax-1re 7429 ax-icn 7430 ax-addcl 7431 ax-addrcl 7432 ax-mulcl 7433 ax-mulrcl 7434 ax-addcom 7435 ax-mulcom 7436 ax-addass 7437 ax-mulass 7438 ax-distr 7439 ax-i2m1 7440 ax-0lt1 7441 ax-1rid 7442 ax-0id 7443 ax-rnegex 7444 ax-precex 7445 ax-cnre 7446 ax-pre-ltirr 7447 ax-pre-ltwlin 7448 ax-pre-lttrn 7449 ax-pre-apti 7450 ax-pre-ltadd 7451 ax-pre-mulgt0 7452 |
| This theorem depends on definitions: df-bi 115 df-3an 926 df-tru 1292 df-fal 1295 df-nf 1395 df-sb 1693 df-eu 1951 df-mo 1952 df-clab 2075 df-cleq 2081 df-clel 2084 df-nfc 2217 df-ne 2256 df-nel 2351 df-ral 2364 df-rex 2365 df-reu 2366 df-rab 2368 df-v 2621 df-sbc 2841 df-dif 3001 df-un 3003 df-in 3005 df-ss 3012 df-pw 3429 df-sn 3450 df-pr 3451 df-op 3453 df-uni 3652 df-br 3844 df-opab 3898 df-id 4118 df-xp 4442 df-rel 4443 df-cnv 4444 df-co 4445 df-dm 4446 df-iota 4975 df-fun 5012 df-fv 5018 df-riota 5600 df-ov 5647 df-oprab 5648 df-mpt2 5649 df-pnf 7514 df-mnf 7515 df-ltxr 7517 df-sub 7645 df-neg 7646 df-reap 8042 df-ap 8049 |
| This theorem is referenced by: addext 8077 mulext 8081 |
| Copyright terms: Public domain | W3C validator |