![]() |
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 2123 | . 2 ⊢ 𝐷 = 𝐴 |
5 | 1, 4 | eqtr4i 2123 | 1 ⊢ 𝐶 = 𝐷 |
Colors of variables: wff set class |
Syntax hints: = wceq 1299 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1391 ax-gen 1393 ax-4 1455 ax-17 1474 ax-ext 2082 |
This theorem depends on definitions: df-bi 116 df-cleq 2093 |
This theorem is referenced by: rabswap 2567 rabbiia 2626 cbvrab 2639 cbvcsb 2959 csbco 2964 cbvrabcsf 3015 un4 3183 in13 3236 in31 3237 in4 3239 indifcom 3269 indir 3272 undir 3273 notrab 3300 dfnul3 3313 rab0 3338 prcom 3546 tprot 3563 tpcoma 3564 tpcomb 3565 tpass 3566 qdassr 3568 pw0 3614 opid 3670 int0 3732 cbviun 3797 cbviin 3798 iunrab 3807 iunin1 3824 cbvopab 3939 cbvopab1 3941 cbvopab2 3942 cbvopab1s 3943 cbvopab2v 3945 unopab 3947 cbvmptf 3962 cbvmpt 3963 iunopab 4141 uniuni 4310 2ordpr 4377 rabxp 4514 fconstmpt 4524 inxp 4611 cnvco 4662 rnmpt 4725 resundi 4768 resundir 4769 resindi 4770 resindir 4771 rescom 4780 resima 4788 imadmrn 4827 cnvimarndm 4839 cnvi 4879 rnun 4883 imaundi 4887 cnvxp 4893 imainrect 4920 imacnvcnv 4939 resdmres 4966 imadmres 4967 mptpreima 4968 cbviota 5029 sb8iota 5031 resdif 5323 cbvriota 5672 dfoprab2 5750 cbvoprab1 5775 cbvoprab2 5776 cbvoprab12 5777 cbvoprab3 5779 cbvmpox 5781 resoprab 5799 caov32 5890 caov31 5892 ofmres 5965 dfopab2 6017 dfxp3 6022 dmmpossx 6027 fmpox 6028 tposco 6102 mapsncnv 6519 cbvixp 6539 xpcomco 6649 sbthlemi6 6778 xp2dju 6975 djuassen 6977 dmaddpi 7034 dmmulpi 7035 dfplpq2 7063 dfmpq2 7064 dmaddpq 7088 dmmulpq 7089 axi2m1 7560 negiso 8571 nummac 9078 decsubi 9096 9t11e99 9163 fzprval 9703 fztpval 9704 sqdivapi 10217 binom2i 10242 4bc2eq6 10361 shftidt2 10445 cji 10515 xrnegiso 10870 cbvsum 10968 fsumrelem 11079 nn0gcdsq 11670 restco 12125 cnmptid 12231 |
Copyright terms: Public domain | W3C validator |