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 2162 | . 2 |
4 | 3eqtr4g.3 | . 2 | |
5 | 3, 4 | syl6eqr 2168 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1316 |
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 1408 ax-gen 1410 ax-4 1472 ax-17 1491 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-cleq 2110 |
This theorem is referenced by: rabbidva2 2647 rabeqf 2650 csbeq1 2978 csbeq2d 2997 csbnestgf 3022 difeq1 3157 difeq2 3158 uneq2 3194 ineq2 3241 dfrab3ss 3324 ifeq1 3447 ifeq2 3448 ifbi 3462 pweq 3483 sneq 3508 csbsng 3554 rabsn 3560 preq1 3570 preq2 3571 tpeq1 3579 tpeq2 3580 tpeq3 3581 prprc1 3601 opeq1 3675 opeq2 3676 oteq1 3684 oteq2 3685 oteq3 3686 csbunig 3714 unieq 3715 inteq 3744 iineq1 3797 iineq2 3800 dfiin2g 3816 iinrabm 3845 iinin1m 3852 iinxprg 3857 opabbid 3963 mpteq12f 3978 suceq 4294 xpeq1 4523 xpeq2 4524 csbxpg 4590 csbdmg 4703 rneq 4736 reseq1 4783 reseq2 4784 csbresg 4792 resindm 4831 resmpt 4837 resmptf 4839 imaeq1 4846 imaeq2 4847 mptcnv 4911 csbrng 4970 dmpropg 4981 rnpropg 4988 cores 5012 cores2 5021 xpcom 5055 iotaeq 5066 iotabi 5067 fntpg 5149 funimaexg 5177 fveq1 5388 fveq2 5389 fvres 5413 csbfv12g 5425 fnimapr 5449 fndmin 5495 fprg 5571 fsnunfv 5589 fsnunres 5590 fliftf 5668 isoini2 5688 riotaeqdv 5699 riotabidv 5700 riotauni 5704 riotabidva 5714 snriota 5727 oveq 5748 oveq1 5749 oveq2 5750 oprabbid 5792 mpoeq123 5798 mpoeq123dva 5800 mpoeq3dva 5803 resmpo 5837 ovres 5878 f1ocnvd 5940 ofeq 5952 ofreq 5953 f1od2 6100 ovtposg 6124 recseq 6171 tfr2a 6186 rdgeq1 6236 rdgeq2 6237 freceq1 6257 freceq2 6258 eceq1 6432 eceq2 6434 qseq1 6445 qseq2 6446 uniqs 6455 ecinxp 6472 qsinxp 6473 erovlem 6489 ixpeq1 6571 supeq1 6841 supeq2 6844 supeq3 6845 supeq123d 6846 infeq1 6866 infeq2 6869 infeq3 6870 infeq123d 6871 infisoti 6887 djueq12 6892 addpiord 7092 mulpiord 7093 00sr 7545 negeq 7923 csbnegg 7928 negsubdi 7986 mulneg1 8125 deceq1 9154 deceq2 9155 xnegeq 9578 fseq1p1m1 9842 frec2uzsucd 10142 frec2uzrdg 10150 frecuzrdgsuc 10155 frecuzrdgg 10157 frecuzrdgsuctlem 10164 seqeq1 10189 seqeq2 10190 seqeq3 10191 seqvalcd 10200 seq3f1olemp 10243 hashprg 10522 shftdm 10562 resqrexlemfp1 10749 negfi 10967 sumeq1 11092 sumeq2 11096 zsumdc 11121 isumss2 11130 fsumsplitsnun 11156 isumclim3 11160 fisumcom2 11175 isumshft 11227 ege2le3 11304 efgt1p2 11328 dfphi2 11823 sloteq 11891 setsslid 11936 metreslem 12476 comet 12595 cnmetdval 12625 |
Copyright terms: Public domain | W3C validator |