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 2223 | . 2 |
4 | 3 | ancoms 266 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wceq 1348 |
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 1440 ax-gen 1442 ax-4 1503 ax-17 1519 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-cleq 2163 |
This theorem is referenced by: sbcied2 2992 csbied2 3096 fun2ssres 5239 fcoi1 5376 fcoi2 5377 funssfv 5520 caovimo 6043 mpomptsx 6173 dmmpossx 6175 fmpox 6176 2ndconst 6198 mpoxopoveq 6216 tfrlemisucaccv 6301 tfr1onlemsucaccv 6317 tfrcllemsucaccv 6330 rdgivallem 6357 nnmass 6463 nnm00 6505 ssenen 6825 fi0 6948 nnnninf2 7099 nnnninfeq2 7101 exmidfodomrlemim 7165 ltexnqq 7357 ltrnqg 7369 nqnq0a 7403 nqnq0m 7404 nq0m0r 7405 nq0a0 7406 addnqprllem 7476 addnqprulem 7477 map2psrprg 7754 rereceu 7838 addid0 8279 nnnn0addcl 9152 zindd 9317 qaddcl 9581 qmulcl 9583 qreccl 9588 xaddpnf1 9790 xaddmnf1 9792 xaddnemnf 9801 xaddnepnf 9802 xaddcom 9805 xnegdi 9812 xaddass 9813 xpncan 9815 xleadd1a 9817 xltadd1 9820 xlt2add 9824 modfzo0difsn 10338 frec2uzrdg 10352 expp1 10470 expnegap0 10471 expcllem 10474 mulexp 10502 expmul 10508 sqoddm1div8 10616 bcpasc 10687 hashfzo 10744 shftfn 10775 reim0b 10813 cjexp 10844 sumsnf 11359 binomlem 11433 prodsnf 11542 ef0lem 11610 dvdsnegb 11757 m1expe 11845 m1expo 11846 m1exp1 11847 flodddiv4 11880 gcdabs 11930 bezoutr1 11975 dvdslcm 12010 lcmeq0 12012 lcmcl 12013 lcmabs 12017 lcmgcdlem 12018 lcmdvds 12020 mulgcddvds 12035 qredeu 12038 divgcdcoprmex 12043 pcge0 12253 pcgcd1 12268 pcadd 12280 pcmpt2 12283 isxmet2d 13101 blfvalps 13138 blssioo 13298 efper 13481 relogbcxpbap 13636 logbgcd1irr 13638 lgsdir 13689 lgsne0 13692 lgsdirnn0 13701 lgsdinn0 13702 trirec0xor 14037 |
Copyright terms: Public domain | W3C validator |