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 2133 | . 2 |
4 | 3 | ancoms 264 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 102 wceq 1284 |
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-5 1376 ax-gen 1378 ax-4 1440 ax-17 1459 ax-ext 2063 |
This theorem depends on definitions: df-bi 115 df-cleq 2074 |
This theorem is referenced by: sbcied2 2851 csbied2 2949 fun2ssres 4963 fcoi1 5090 fcoi2 5091 funssfv 5220 caovimo 5714 mpt2mptsx 5843 dmmpt2ssx 5845 fmpt2x 5846 2ndconst 5863 mpt2xopoveq 5878 tfrlemisucaccv 5962 rdgivallem 5991 nnmass 6089 nnm00 6125 ltexnqq 6598 ltrnqg 6610 nqnq0a 6644 nqnq0m 6645 nq0m0r 6646 nq0a0 6647 addnqprllem 6717 addnqprulem 6718 rereceu 7055 addid0 7477 nnnn0addcl 8318 zindd 8465 qaddcl 8720 qmulcl 8722 qreccl 8727 modfzo0difsn 9397 frec2uzrdg 9411 expp1 9483 expnegap0 9484 expcllem 9487 mulexp 9515 expmul 9521 sqoddm1div8 9625 bcpasc 9693 shftfn 9712 reim0b 9749 cjexp 9780 dvdsnegb 10212 m1expe 10299 m1expo 10300 m1exp1 10301 flodddiv4 10334 gcdabs 10379 bezoutr1 10422 dvdslcm 10451 lcmeq0 10453 lcmcl 10454 lcmabs 10458 lcmgcdlem 10459 lcmdvds 10461 mulgcddvds 10476 qredeu 10479 divgcdcoprmex 10484 |
Copyright terms: Public domain | W3C validator |