Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3eqtr4g | GIF 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 2202 | . 2 ⊢ (𝜑 → 𝐶 = 𝐵) |
4 | 3eqtr4g.3 | . 2 ⊢ 𝐷 = 𝐵 | |
5 | 3, 4 | eqtr4di 2208 | 1 ⊢ (𝜑 → 𝐶 = 𝐷) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1335 |
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 1427 ax-gen 1429 ax-4 1490 ax-17 1506 ax-ext 2139 |
This theorem depends on definitions: df-bi 116 df-cleq 2150 |
This theorem is referenced by: rabbidva2 2699 rabeqf 2702 csbeq1 3034 csbeq2 3055 csbeq2d 3056 csbnestgf 3083 difeq1 3218 difeq2 3219 uneq2 3255 ineq2 3302 dfrab3ss 3385 ifeq1 3508 ifeq2 3509 ifbi 3525 pweq 3546 sneq 3571 csbsng 3620 rabsn 3626 preq1 3636 preq2 3637 tpeq1 3645 tpeq2 3646 tpeq3 3647 prprc1 3667 opeq1 3741 opeq2 3742 oteq1 3750 oteq2 3751 oteq3 3752 csbunig 3780 unieq 3781 inteq 3810 iineq1 3863 iineq2 3866 dfiin2g 3882 iinrabm 3911 iinin1m 3918 iinxprg 3923 opabbid 4029 mpteq12f 4044 suceq 4362 xpeq1 4600 xpeq2 4601 csbxpg 4667 csbdmg 4780 rneq 4813 reseq1 4860 reseq2 4861 csbresg 4869 resindm 4908 resmpt 4914 resmptf 4916 imaeq1 4923 imaeq2 4924 mptcnv 4988 csbrng 5047 dmpropg 5058 rnpropg 5065 cores 5089 cores2 5098 xpcom 5132 iotaeq 5143 iotabi 5144 fntpg 5226 funimaexg 5254 fveq1 5467 fveq2 5468 fvres 5492 csbfv12g 5504 fnimapr 5528 fndmin 5574 fprg 5650 fsnunfv 5668 fsnunres 5669 fliftf 5749 isoini2 5769 riotaeqdv 5781 riotabidv 5782 riotauni 5786 riotabidva 5796 snriota 5809 oveq 5830 oveq1 5831 oveq2 5832 oprabbid 5874 mpoeq123 5880 mpoeq123dva 5882 mpoeq3dva 5885 resmpo 5919 ovres 5960 f1ocnvd 6022 ofeq 6034 ofreq 6035 f1od2 6182 ovtposg 6206 recseq 6253 tfr2a 6268 rdgeq1 6318 rdgeq2 6319 freceq1 6339 freceq2 6340 eceq1 6515 eceq2 6517 qseq1 6528 qseq2 6529 uniqs 6538 ecinxp 6555 qsinxp 6556 erovlem 6572 ixpeq1 6654 supeq1 6930 supeq2 6933 supeq3 6934 supeq123d 6935 infeq1 6955 infeq2 6958 infeq3 6959 infeq123d 6960 infisoti 6976 djueq12 6983 addpiord 7236 mulpiord 7237 00sr 7689 negeq 8068 csbnegg 8073 negsubdi 8131 mulneg1 8270 deceq1 9299 deceq2 9300 xnegeq 9731 fseq1p1m1 9996 frec2uzsucd 10300 frec2uzrdg 10308 frecuzrdgsuc 10313 frecuzrdgg 10315 frecuzrdgsuctlem 10322 seqeq1 10347 seqeq2 10348 seqeq3 10349 seqvalcd 10358 seq3f1olemp 10401 hashprg 10682 shftdm 10722 resqrexlemfp1 10909 negfi 11127 sumeq1 11252 sumeq2 11256 zsumdc 11281 isumss2 11290 fsumsplitsnun 11316 isumclim3 11320 fisumcom2 11335 isumshft 11387 prodeq1f 11449 prodeq2w 11453 prodeq2 11454 zproddc 11476 fprodm1s 11498 fprodp1s 11499 fprodcom2fi 11523 fprodsplitf 11529 ege2le3 11568 efgt1p2 11592 dfphi2 12094 prmdiveq 12110 sloteq 12195 setsslid 12240 metreslem 12780 comet 12899 cnmetdval 12929 redcwlpolemeq1 13625 |
Copyright terms: Public domain | W3C validator |