![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3eqtr4i | GIF version |
Description: An inference from three chained equalities. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
3eqtr4i.1 | ⊢ 𝐴 = 𝐵 |
3eqtr4i.2 | ⊢ 𝐶 = 𝐴 |
3eqtr4i.3 | ⊢ 𝐷 = 𝐵 |
Ref | Expression |
---|---|
3eqtr4i | ⊢ 𝐶 = 𝐷 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr4i.2 | . 2 ⊢ 𝐶 = 𝐴 | |
2 | 3eqtr4i.3 | . . 3 ⊢ 𝐷 = 𝐵 | |
3 | 3eqtr4i.1 | . . 3 ⊢ 𝐴 = 𝐵 | |
4 | 2, 3 | eqtr4i 2201 | . 2 ⊢ 𝐷 = 𝐴 |
5 | 1, 4 | eqtr4i 2201 | 1 ⊢ 𝐶 = 𝐷 |
Colors of variables: wff set class |
Syntax hints: = wceq 1353 |
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 1447 ax-gen 1449 ax-4 1510 ax-17 1526 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 |
This theorem is referenced by: rabswap 2656 rabbiia 2724 cbvrab 2737 cbvcsbw 3063 cbvcsb 3064 csbco 3069 csbcow 3070 cbvrabcsf 3124 un4 3297 in13 3350 in31 3351 in4 3353 indifcom 3383 indir 3386 undir 3387 notrab 3414 dfnul3 3427 rab0 3453 prcom 3670 tprot 3687 tpcoma 3688 tpcomb 3689 tpass 3690 qdassr 3692 pw0 3741 opid 3798 int0 3860 cbviun 3925 cbviin 3926 iunrab 3936 iunin1 3953 cbvopab 4076 cbvopab1 4078 cbvopab2 4079 cbvopab1s 4080 cbvopab2v 4082 unopab 4084 cbvmptf 4099 cbvmpt 4100 iunopab 4283 uniuni 4453 2ordpr 4525 rabxp 4665 fconstmpt 4675 inxp 4763 cnvco 4814 rnmpt 4877 resundi 4922 resundir 4923 resindi 4924 resindir 4925 rescom 4934 resima 4942 imadmrn 4982 cnvimarndm 4994 cnvi 5035 rnun 5039 imaundi 5043 cnvxp 5049 imainrect 5076 imacnvcnv 5095 resdmres 5122 imadmres 5123 mptpreima 5124 cbviota 5185 sb8iota 5187 resdif 5485 cbvriota 5844 dfoprab2 5925 cbvoprab1 5950 cbvoprab2 5951 cbvoprab12 5952 cbvoprab3 5954 cbvmpox 5956 resoprab 5974 caov32 6065 caov31 6067 ofmres 6140 dfopab2 6193 dfxp3 6198 dmmpossx 6203 fmpox 6204 tposco 6279 mapsncnv 6698 cbvixp 6718 xpcomco 6829 sbthlemi6 6964 xp2dju 7217 djuassen 7219 dmaddpi 7327 dmmulpi 7328 dfplpq2 7356 dfmpq2 7357 dmaddpq 7381 dmmulpq 7382 axi2m1 7877 negiso 8915 nummac 9431 decsubi 9449 9t11e99 9516 fzprval 10085 fztpval 10086 sqdivapi 10607 binom2i 10632 4bc2eq6 10757 shftidt2 10844 cji 10914 xrnegiso 11273 cbvsum 11371 fsumrelem 11482 cbvprod 11569 nn0gcdsq 12203 rmodislmod 13447 cnfldsub 13609 dvdsrzring 13633 restco 13814 cnmptid 13921 sincos3rdpi 14404 lgsdir2lem5 14573 2lgsoddprmlem3d 14598 if0ab 14697 |
Copyright terms: Public domain | W3C validator |