![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3eqtr4g | Unicode version |
Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
3eqtr4g.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3eqtr4g.2 |
![]() ![]() ![]() ![]() |
3eqtr4g.3 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3eqtr4g |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr4g.2 |
. . 3
![]() ![]() ![]() ![]() | |
2 | 3eqtr4g.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | eqtrid 2238 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3eqtr4g.3 |
. 2
![]() ![]() ![]() ![]() | |
5 | 3, 4 | eqtr4di 2244 |
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 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-gen 1460 ax-4 1521 ax-17 1537 ax-ext 2175 |
This theorem depends on definitions: df-bi 117 df-cleq 2186 |
This theorem is referenced by: rabbidva2 2747 rabeqf 2750 csbeq1 3083 csbeq2 3104 csbeq2d 3105 csbnestgf 3133 difeq1 3270 difeq2 3271 uneq2 3307 ineq2 3354 dfrab3ss 3437 ifeq1 3560 ifeq2 3561 ifbi 3577 pweq 3604 sneq 3629 csbsng 3679 rabsn 3685 preq1 3695 preq2 3696 tpeq1 3704 tpeq2 3705 tpeq3 3706 prprc1 3726 opeq1 3804 opeq2 3805 oteq1 3813 oteq2 3814 oteq3 3815 csbunig 3843 unieq 3844 inteq 3873 iineq1 3926 iineq2 3929 dfiin2g 3945 iinrabm 3975 iinin1m 3982 iinxprg 3987 opabbid 4094 mpteq12f 4109 suceq 4433 xpeq1 4673 xpeq2 4674 csbxpg 4740 csbdmg 4856 rneq 4889 reseq1 4936 reseq2 4937 csbresg 4945 resindm 4984 resmpt 4990 resmptf 4992 imaeq1 5000 imaeq2 5001 mptcnv 5068 csbrng 5127 dmpropg 5138 rnpropg 5145 cores 5169 cores2 5178 xpcom 5212 iotaeq 5223 iotabi 5224 fntpg 5310 funimaexg 5338 fveq1 5553 fveq2 5554 fvres 5578 csbfv12g 5592 fnimapr 5617 fndmin 5665 fprg 5741 fsnunfv 5759 fsnunres 5760 fliftf 5842 isoini2 5862 riotaeqdv 5874 riotabidv 5875 riotauni 5880 riotabidva 5890 snriota 5903 oveq 5924 oveq1 5925 oveq2 5926 oprabbid 5971 mpoeq123 5977 mpoeq123dva 5979 mpoeq3dva 5982 resmpo 6016 ovres 6058 f1ocnvd 6120 ofeqd 6132 ofeq 6133 ofreq 6134 f1od2 6288 ovtposg 6312 recseq 6359 tfr2a 6374 rdgeq1 6424 rdgeq2 6425 freceq1 6445 freceq2 6446 eceq1 6622 eceq2 6624 qseq1 6637 qseq2 6638 uniqs 6647 ecinxp 6664 qsinxp 6665 erovlem 6681 ixpeq1 6763 supeq1 7045 supeq2 7048 supeq3 7049 supeq123d 7050 infeq1 7070 infeq2 7073 infeq3 7074 infeq123d 7075 infisoti 7091 djueq12 7098 addpiord 7376 mulpiord 7377 00sr 7829 negeq 8212 csbnegg 8217 negsubdi 8275 mulneg1 8414 deceq1 9452 deceq2 9453 xnegeq 9893 fseq1p1m1 10160 frec2uzsucd 10472 frec2uzrdg 10480 frecuzrdgsuc 10485 frecuzrdgg 10487 frecuzrdgsuctlem 10494 seqeq1 10521 seqeq2 10522 seqeq3 10523 seqvalcd 10532 seq3f1olemp 10586 hashprg 10879 shftdm 10966 resqrexlemfp1 11153 negfi 11371 sumeq1 11498 sumeq2 11502 zsumdc 11527 isumss2 11536 fsumsplitsnun 11562 isumclim3 11566 fisumcom2 11581 isumshft 11633 prodeq1f 11695 prodeq2w 11699 prodeq2 11700 zproddc 11722 fprodm1s 11744 fprodp1s 11745 fprodcom2fi 11769 fprodsplitf 11775 ege2le3 11814 efgt1p2 11838 dfphi2 12358 prmdiveq 12374 pceulem 12432 sloteq 12623 setsslid 12669 ressval2 12684 ecqusaddd 13308 ringidvalg 13457 zrhpropd 14114 metreslem 14548 comet 14667 cnmetdval 14697 lgsdi 15153 lgseisenlem2 15187 redcwlpolemeq1 15544 |
Copyright terms: Public domain | W3C validator |