![]() |
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 2193 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | ancoms 266 |
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 105 ax-ia2 106 ax-ia3 107 ax-5 1424 ax-gen 1426 ax-4 1488 ax-17 1507 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-cleq 2133 |
This theorem is referenced by: sbcied2 2950 csbied2 3052 fun2ssres 5174 fcoi1 5311 fcoi2 5312 funssfv 5455 caovimo 5972 mpomptsx 6103 dmmpossx 6105 fmpox 6106 2ndconst 6127 mpoxopoveq 6145 tfrlemisucaccv 6230 tfr1onlemsucaccv 6246 tfrcllemsucaccv 6259 rdgivallem 6286 nnmass 6391 nnm00 6433 ssenen 6753 fi0 6871 exmidfodomrlemim 7074 ltexnqq 7240 ltrnqg 7252 nqnq0a 7286 nqnq0m 7287 nq0m0r 7288 nq0a0 7289 addnqprllem 7359 addnqprulem 7360 map2psrprg 7637 rereceu 7721 addid0 8159 nnnn0addcl 9031 zindd 9193 qaddcl 9454 qmulcl 9456 qreccl 9461 xaddpnf1 9659 xaddmnf1 9661 xaddnemnf 9670 xaddnepnf 9671 xaddcom 9674 xnegdi 9681 xaddass 9682 xpncan 9684 xleadd1a 9686 xltadd1 9689 xlt2add 9693 modfzo0difsn 10199 frec2uzrdg 10213 expp1 10331 expnegap0 10332 expcllem 10335 mulexp 10363 expmul 10369 sqoddm1div8 10475 bcpasc 10544 hashfzo 10600 shftfn 10628 reim0b 10666 cjexp 10697 sumsnf 11210 binomlem 11284 ef0lem 11403 dvdsnegb 11546 m1expe 11632 m1expo 11633 m1exp1 11634 flodddiv4 11667 gcdabs 11712 bezoutr1 11757 dvdslcm 11786 lcmeq0 11788 lcmcl 11789 lcmabs 11793 lcmgcdlem 11794 lcmdvds 11796 mulgcddvds 11811 qredeu 11814 divgcdcoprmex 11819 isxmet2d 12556 blfvalps 12593 blssioo 12753 efper 12936 relogbcxpbap 13090 logbgcd1irr 13092 trirec0xor 13413 |
Copyright terms: Public domain | W3C validator |