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 | syl5eq 2209 | . 2 |
4 | 3eqtr4g.3 | . 2 | |
5 | 3, 4 | eqtr4di 2215 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1342 |
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 1434 ax-gen 1436 ax-4 1497 ax-17 1513 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-cleq 2157 |
This theorem is referenced by: rabbidva2 2708 rabeqf 2711 csbeq1 3043 csbeq2 3064 csbeq2d 3065 csbnestgf 3092 difeq1 3228 difeq2 3229 uneq2 3265 ineq2 3312 dfrab3ss 3395 ifeq1 3518 ifeq2 3519 ifbi 3535 pweq 3556 sneq 3581 csbsng 3631 rabsn 3637 preq1 3647 preq2 3648 tpeq1 3656 tpeq2 3657 tpeq3 3658 prprc1 3678 opeq1 3752 opeq2 3753 oteq1 3761 oteq2 3762 oteq3 3763 csbunig 3791 unieq 3792 inteq 3821 iineq1 3874 iineq2 3877 dfiin2g 3893 iinrabm 3922 iinin1m 3929 iinxprg 3934 opabbid 4041 mpteq12f 4056 suceq 4374 xpeq1 4612 xpeq2 4613 csbxpg 4679 csbdmg 4792 rneq 4825 reseq1 4872 reseq2 4873 csbresg 4881 resindm 4920 resmpt 4926 resmptf 4928 imaeq1 4935 imaeq2 4936 mptcnv 5000 csbrng 5059 dmpropg 5070 rnpropg 5077 cores 5101 cores2 5110 xpcom 5144 iotaeq 5155 iotabi 5156 fntpg 5238 funimaexg 5266 fveq1 5479 fveq2 5480 fvres 5504 csbfv12g 5516 fnimapr 5540 fndmin 5586 fprg 5662 fsnunfv 5680 fsnunres 5681 fliftf 5761 isoini2 5781 riotaeqdv 5793 riotabidv 5794 riotauni 5798 riotabidva 5808 snriota 5821 oveq 5842 oveq1 5843 oveq2 5844 oprabbid 5886 mpoeq123 5892 mpoeq123dva 5894 mpoeq3dva 5897 resmpo 5931 ovres 5972 f1ocnvd 6034 ofeq 6046 ofreq 6047 f1od2 6194 ovtposg 6218 recseq 6265 tfr2a 6280 rdgeq1 6330 rdgeq2 6331 freceq1 6351 freceq2 6352 eceq1 6527 eceq2 6529 qseq1 6540 qseq2 6541 uniqs 6550 ecinxp 6567 qsinxp 6568 erovlem 6584 ixpeq1 6666 supeq1 6942 supeq2 6945 supeq3 6946 supeq123d 6947 infeq1 6967 infeq2 6970 infeq3 6971 infeq123d 6972 infisoti 6988 djueq12 6995 addpiord 7248 mulpiord 7249 00sr 7701 negeq 8082 csbnegg 8087 negsubdi 8145 mulneg1 8284 deceq1 9317 deceq2 9318 xnegeq 9754 fseq1p1m1 10019 frec2uzsucd 10326 frec2uzrdg 10334 frecuzrdgsuc 10339 frecuzrdgg 10341 frecuzrdgsuctlem 10348 seqeq1 10373 seqeq2 10374 seqeq3 10375 seqvalcd 10384 seq3f1olemp 10427 hashprg 10710 shftdm 10750 resqrexlemfp1 10937 negfi 11155 sumeq1 11282 sumeq2 11286 zsumdc 11311 isumss2 11320 fsumsplitsnun 11346 isumclim3 11350 fisumcom2 11365 isumshft 11417 prodeq1f 11479 prodeq2w 11483 prodeq2 11484 zproddc 11506 fprodm1s 11528 fprodp1s 11529 fprodcom2fi 11553 fprodsplitf 11559 ege2le3 11598 efgt1p2 11622 dfphi2 12131 prmdiveq 12147 pceulem 12205 sloteq 12342 setsslid 12387 metreslem 12927 comet 13046 cnmetdval 13076 redcwlpolemeq1 13774 |
Copyright terms: Public domain | W3C validator |