![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sylan9eqr | Unicode version |
Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.) |
Ref | Expression |
---|---|
sylan9eqr.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
sylan9eqr.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
sylan9eqr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylan9eqr.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sylan9eqr.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylan9eq 2242 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | ancoms 268 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-gen 1460 ax-4 1521 ax-17 1537 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-cleq 2182 |
This theorem is referenced by: sbcied2 3015 csbied2 3119 fun2ssres 5274 fcoi1 5411 fcoi2 5412 funssfv 5556 caovimo 6085 mpomptsx 6216 dmmpossx 6218 fmpox 6219 2ndconst 6241 mpoxopoveq 6259 tfrlemisucaccv 6344 tfr1onlemsucaccv 6360 tfrcllemsucaccv 6373 rdgivallem 6400 nnmass 6506 nnm00 6549 ssenen 6869 fi0 6992 nnnninf2 7143 nnnninfeq2 7145 exmidfodomrlemim 7218 ltexnqq 7425 ltrnqg 7437 nqnq0a 7471 nqnq0m 7472 nq0m0r 7473 nq0a0 7474 addnqprllem 7544 addnqprulem 7545 map2psrprg 7822 rereceu 7906 addid0 8348 nnnn0addcl 9224 zindd 9389 qaddcl 9653 qmulcl 9655 qreccl 9660 xaddpnf1 9864 xaddmnf1 9866 xaddnemnf 9875 xaddnepnf 9876 xaddcom 9879 xnegdi 9886 xaddass 9887 xpncan 9889 xleadd1a 9891 xltadd1 9894 xlt2add 9898 modfzo0difsn 10413 frec2uzrdg 10427 expp1 10545 expnegap0 10546 expcllem 10549 mulexp 10577 expmul 10583 sqoddm1div8 10692 bcpasc 10764 hashfzo 10820 shftfn 10851 reim0b 10889 cjexp 10920 sumsnf 11435 binomlem 11509 prodsnf 11618 ef0lem 11686 dvdsnegb 11833 m1expe 11922 m1expo 11923 m1exp1 11924 flodddiv4 11957 gcdabs 12007 bezoutr1 12052 dvdslcm 12087 lcmeq0 12089 lcmcl 12090 lcmabs 12094 lcmgcdlem 12095 lcmdvds 12097 mulgcddvds 12112 qredeu 12115 divgcdcoprmex 12120 pcge0 12330 pcgcd1 12345 pcadd 12357 pcmpt2 12360 mulgfvalg 13029 mulgnn0subcl 13041 mulgnn0z 13055 f1ghm0to0 13172 srgmulgass 13304 srgpcomp 13305 ringinvnzdiv 13363 lmodvsmmulgdi 13600 znval 13893 isxmet2d 14245 blfvalps 14282 blssioo 14442 efper 14625 relogbcxpbap 14780 logbgcd1irr 14782 lgsdir 14833 lgsne0 14836 lgsdirnn0 14845 lgsdinn0 14846 trirec0xor 15191 |
Copyright terms: Public domain | W3C validator |