![]() |
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 2152 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | ancoms 266 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1391 ax-gen 1393 ax-4 1455 ax-17 1474 ax-ext 2082 |
This theorem depends on definitions: df-bi 116 df-cleq 2093 |
This theorem is referenced by: sbcied2 2898 csbied2 2997 fun2ssres 5102 fcoi1 5239 fcoi2 5240 funssfv 5379 caovimo 5896 mpomptsx 6025 dmmpossx 6027 fmpox 6028 2ndconst 6049 mpoxopoveq 6067 tfrlemisucaccv 6152 tfr1onlemsucaccv 6168 tfrcllemsucaccv 6181 rdgivallem 6208 nnmass 6313 nnm00 6355 ssenen 6674 exmidfodomrlemim 6966 ltexnqq 7117 ltrnqg 7129 nqnq0a 7163 nqnq0m 7164 nq0m0r 7165 nq0a0 7166 addnqprllem 7236 addnqprulem 7237 rereceu 7574 addid0 8002 nnnn0addcl 8859 zindd 9021 qaddcl 9277 qmulcl 9279 qreccl 9284 xaddpnf1 9470 xaddmnf1 9472 xaddnemnf 9481 xaddnepnf 9482 xaddcom 9485 xnegdi 9492 xaddass 9493 xpncan 9495 xleadd1a 9497 xltadd1 9500 xlt2add 9504 modfzo0difsn 10009 frec2uzrdg 10023 expp1 10141 expnegap0 10142 expcllem 10145 mulexp 10173 expmul 10179 sqoddm1div8 10285 bcpasc 10353 hashfzo 10409 shftfn 10437 reim0b 10475 cjexp 10506 sumsnf 11017 binomlem 11091 ef0lem 11164 dvdsnegb 11305 m1expe 11391 m1expo 11392 m1exp1 11393 flodddiv4 11426 gcdabs 11471 bezoutr1 11514 dvdslcm 11543 lcmeq0 11545 lcmcl 11546 lcmabs 11550 lcmgcdlem 11551 lcmdvds 11553 mulgcddvds 11568 qredeu 11571 divgcdcoprmex 11576 isxmet2d 12276 blfvalps 12313 blssioo 12464 |
Copyright terms: Public domain | W3C validator |