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 2141 | . 2 ⊢ 𝐷 = 𝐴 |
5 | 1, 4 | eqtr4i 2141 | 1 ⊢ 𝐶 = 𝐷 |
Colors of variables: wff set class |
Syntax hints: = 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: rabswap 2586 rabbiia 2645 cbvrab 2658 cbvcsb 2979 csbco 2984 cbvrabcsf 3035 un4 3206 in13 3259 in31 3260 in4 3262 indifcom 3292 indir 3295 undir 3296 notrab 3323 dfnul3 3336 rab0 3361 prcom 3569 tprot 3586 tpcoma 3587 tpcomb 3588 tpass 3589 qdassr 3591 pw0 3637 opid 3693 int0 3755 cbviun 3820 cbviin 3821 iunrab 3830 iunin1 3847 cbvopab 3969 cbvopab1 3971 cbvopab2 3972 cbvopab1s 3973 cbvopab2v 3975 unopab 3977 cbvmptf 3992 cbvmpt 3993 iunopab 4173 uniuni 4342 2ordpr 4409 rabxp 4546 fconstmpt 4556 inxp 4643 cnvco 4694 rnmpt 4757 resundi 4802 resundir 4803 resindi 4804 resindir 4805 rescom 4814 resima 4822 imadmrn 4861 cnvimarndm 4873 cnvi 4913 rnun 4917 imaundi 4921 cnvxp 4927 imainrect 4954 imacnvcnv 4973 resdmres 5000 imadmres 5001 mptpreima 5002 cbviota 5063 sb8iota 5065 resdif 5357 cbvriota 5708 dfoprab2 5786 cbvoprab1 5811 cbvoprab2 5812 cbvoprab12 5813 cbvoprab3 5815 cbvmpox 5817 resoprab 5835 caov32 5926 caov31 5928 ofmres 6002 dfopab2 6055 dfxp3 6060 dmmpossx 6065 fmpox 6066 tposco 6140 mapsncnv 6557 cbvixp 6577 xpcomco 6688 sbthlemi6 6818 xp2dju 7039 djuassen 7041 dmaddpi 7101 dmmulpi 7102 dfplpq2 7130 dfmpq2 7131 dmaddpq 7155 dmmulpq 7156 axi2m1 7651 negiso 8681 nummac 9194 decsubi 9212 9t11e99 9279 fzprval 9830 fztpval 9831 sqdivapi 10344 binom2i 10369 4bc2eq6 10488 shftidt2 10572 cji 10642 xrnegiso 10999 cbvsum 11097 fsumrelem 11208 nn0gcdsq 11805 restco 12270 cnmptid 12377 sincos3rdpi 12851 |
Copyright terms: Public domain | W3C validator |