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 | eqtrid 2215 | . 2 ⊢ (𝜑 → 𝐶 = 𝐵) |
4 | 3eqtr4g.3 | . 2 ⊢ 𝐷 = 𝐵 | |
5 | 3, 4 | eqtr4di 2221 | 1 ⊢ (𝜑 → 𝐶 = 𝐷) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1348 |
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 1440 ax-gen 1442 ax-4 1503 ax-17 1519 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-cleq 2163 |
This theorem is referenced by: rabbidva2 2717 rabeqf 2720 csbeq1 3052 csbeq2 3073 csbeq2d 3074 csbnestgf 3101 difeq1 3238 difeq2 3239 uneq2 3275 ineq2 3322 dfrab3ss 3405 ifeq1 3529 ifeq2 3530 ifbi 3546 pweq 3569 sneq 3594 csbsng 3644 rabsn 3650 preq1 3660 preq2 3661 tpeq1 3669 tpeq2 3670 tpeq3 3671 prprc1 3691 opeq1 3765 opeq2 3766 oteq1 3774 oteq2 3775 oteq3 3776 csbunig 3804 unieq 3805 inteq 3834 iineq1 3887 iineq2 3890 dfiin2g 3906 iinrabm 3935 iinin1m 3942 iinxprg 3947 opabbid 4054 mpteq12f 4069 suceq 4387 xpeq1 4625 xpeq2 4626 csbxpg 4692 csbdmg 4805 rneq 4838 reseq1 4885 reseq2 4886 csbresg 4894 resindm 4933 resmpt 4939 resmptf 4941 imaeq1 4948 imaeq2 4949 mptcnv 5013 csbrng 5072 dmpropg 5083 rnpropg 5090 cores 5114 cores2 5123 xpcom 5157 iotaeq 5168 iotabi 5169 fntpg 5254 funimaexg 5282 fveq1 5495 fveq2 5496 fvres 5520 csbfv12g 5532 fnimapr 5556 fndmin 5603 fprg 5679 fsnunfv 5697 fsnunres 5698 fliftf 5778 isoini2 5798 riotaeqdv 5810 riotabidv 5811 riotauni 5815 riotabidva 5825 snriota 5838 oveq 5859 oveq1 5860 oveq2 5861 oprabbid 5906 mpoeq123 5912 mpoeq123dva 5914 mpoeq3dva 5917 resmpo 5951 ovres 5992 f1ocnvd 6051 ofeq 6063 ofreq 6064 f1od2 6214 ovtposg 6238 recseq 6285 tfr2a 6300 rdgeq1 6350 rdgeq2 6351 freceq1 6371 freceq2 6372 eceq1 6548 eceq2 6550 qseq1 6561 qseq2 6562 uniqs 6571 ecinxp 6588 qsinxp 6589 erovlem 6605 ixpeq1 6687 supeq1 6963 supeq2 6966 supeq3 6967 supeq123d 6968 infeq1 6988 infeq2 6991 infeq3 6992 infeq123d 6993 infisoti 7009 djueq12 7016 addpiord 7278 mulpiord 7279 00sr 7731 negeq 8112 csbnegg 8117 negsubdi 8175 mulneg1 8314 deceq1 9347 deceq2 9348 xnegeq 9784 fseq1p1m1 10050 frec2uzsucd 10357 frec2uzrdg 10365 frecuzrdgsuc 10370 frecuzrdgg 10372 frecuzrdgsuctlem 10379 seqeq1 10404 seqeq2 10405 seqeq3 10406 seqvalcd 10415 seq3f1olemp 10458 hashprg 10743 shftdm 10786 resqrexlemfp1 10973 negfi 11191 sumeq1 11318 sumeq2 11322 zsumdc 11347 isumss2 11356 fsumsplitsnun 11382 isumclim3 11386 fisumcom2 11401 isumshft 11453 prodeq1f 11515 prodeq2w 11519 prodeq2 11520 zproddc 11542 fprodm1s 11564 fprodp1s 11565 fprodcom2fi 11589 fprodsplitf 11595 ege2le3 11634 efgt1p2 11658 dfphi2 12174 prmdiveq 12190 pceulem 12248 sloteq 12421 setsslid 12466 metreslem 13174 comet 13293 cnmetdval 13323 lgsdi 13732 redcwlpolemeq1 14086 |
Copyright terms: Public domain | W3C validator |