![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqtr4di | Unicode version |
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqtr4di.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
eqtr4di.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
eqtr4di |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqtr4di.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | eqtr4di.2 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 2 | eqcomi 2158 |
. 2
![]() ![]() ![]() ![]() |
4 | 1, 3 | eqtrdi 2203 |
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 1487 ax-17 1503 ax-ext 2136 |
This theorem depends on definitions: df-bi 116 df-cleq 2147 |
This theorem is referenced by: 3eqtr4g 2212 rabxmdc 3421 relop 4729 csbcnvg 4763 dfiun3g 4836 dfiin3g 4837 resima2 4893 relcnvfld 5112 uniabio 5138 fntpg 5219 dffn5im 5507 dfimafn2 5511 fncnvima2 5581 fmptcof 5627 fcoconst 5631 fnasrng 5640 ffnov 5915 fnovim 5919 fnrnov 5956 foov 5957 funimassov 5960 ovelimab 5961 ofc12 6042 caofinvl 6044 dftpos3 6199 tfr0dm 6259 rdgisucinc 6322 oasuc 6400 ecinxp 6544 phplem1 6786 exmidpw 6842 exmidpweq 6843 unfiin 6859 fidcenumlemr 6888 0ct 7037 ctmlemr 7038 exmidaclem 7122 indpi 7241 nqnq0pi 7337 nq0m0r 7355 addnqpr1 7461 recexgt0sr 7672 suplocsrlempr 7706 recidpipr 7755 recidpirq 7757 axrnegex 7778 nntopi 7793 cnref1o 9537 fztp 9958 fseq1m1p1 9975 frecuzrdgrrn 10285 frecuzrdgsuc 10291 frecuzrdgsuctlem 10300 seq3val 10335 seqvalcd 10336 fser0const 10393 mulexpzap 10437 expaddzap 10441 bcp1m1 10616 cjexp 10770 rexuz3 10867 bdtri 11116 climconst 11164 sumfct 11248 zsumdc 11258 fsum3 11261 sum0 11262 fsumcnv 11311 mertenslem2 11410 zproddc 11453 fprodseq 11457 prod0 11459 prod1dc 11460 prodfct 11461 fprodcnv 11499 ef0lem 11534 efzval 11557 efival 11606 sinbnd 11626 cosbnd 11627 eucalgval 11902 eucalginv 11904 eucalglt 11905 eucalgcvga 11906 eucalg 11907 sqpweven 12020 2sqpwodd 12021 dfphi2 12063 phimullem 12068 ennnfonelemhdmp1 12089 ennnfonelemkh 12092 ressid2 12188 ressval2 12189 topnvalg 12302 istps 12369 cldval 12438 ntrfval 12439 clsfval 12440 neifval 12479 restbasg 12507 tgrest 12508 txval 12594 upxp 12611 uptx 12613 txrest 12615 lmcn2 12619 cnmpt2t 12632 cnmpt2res 12636 imasnopn 12638 psmetxrge0 12671 xmetge0 12704 isxms 12790 isms 12792 bdxmet 12840 qtopbasss 12860 cnblcld 12874 negfcncf 12928 dvfvalap 12989 eldvap 12990 dvidlemap 12999 dvexp2 13015 dvrecap 13016 dveflem 13026 sin0pilem1 13041 ptolemy 13084 coskpi 13108 logbrec 13216 nninfsellemqall 13528 |
Copyright terms: Public domain | W3C validator |