![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3eqtr3i | Structured version Visualization version GIF version |
Description: An inference from three chained equalities. (Contributed by NM, 6-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
3eqtr3i.1 | ⊢ 𝐴 = 𝐵 |
3eqtr3i.2 | ⊢ 𝐴 = 𝐶 |
3eqtr3i.3 | ⊢ 𝐵 = 𝐷 |
Ref | Expression |
---|---|
3eqtr3i | ⊢ 𝐶 = 𝐷 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr3i.1 | . . 3 ⊢ 𝐴 = 𝐵 | |
2 | 3eqtr3i.2 | . . 3 ⊢ 𝐴 = 𝐶 | |
3 | 1, 2 | eqtr3i 2804 | . 2 ⊢ 𝐵 = 𝐶 |
4 | 3eqtr3i.3 | . 2 ⊢ 𝐵 = 𝐷 | |
5 | 3, 4 | eqtr3i 2804 | 1 ⊢ 𝐶 = 𝐷 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1507 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-9 2059 ax-ext 2750 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1743 df-cleq 2771 |
This theorem is referenced by: un12 4034 in12 4086 indif1 4137 difundi 4145 difundir 4146 difindi 4147 difindir 4148 dif32 4156 csbvarg 4268 undif1 4308 resmpt3 5753 xp0 5857 fresaunres2 6381 fvsnun1OLD 6773 caov12 7194 caov13 7196 caov411 7198 caovdir 7200 orduniss2 7366 fparlem3 7619 fparlem4 7620 hartogslem1 8803 kmlem3 9374 djuassen 9404 xpdjuen 9405 halfnq 10198 reclem3pr 10271 addcmpblnr 10291 ltsrpr 10299 pn0sr 10323 sqgt0sr 10328 map2psrpr 10332 negsubdii 10774 halfpm6th 11671 decmul1OLD 11980 i4 13385 nn0opthlem1 13446 fac4 13459 imi 14380 bpoly3 15275 ef01bndlem 15400 bitsres 15685 gcdaddmlem 15735 modsubi 16267 gcdmodi 16269 numexpp1 16273 karatsuba 16279 oppgcntr 18267 frgpuplem 18661 ressmpladd 19954 ressmplmul 19955 ressmplvsca 19956 ltbwe 19969 ressply1add 20104 ressply1mul 20105 ressply1vsca 20106 sn0cld 21405 qtopres 22013 itg1addlem5 24007 cospi 24764 sincos4thpi 24805 sincos3rdpi 24808 dvlog 24938 dvlog2 24940 dvsqrt 25027 dvcnsqrt 25029 ang180lem3 25093 1cubrlem 25123 mcubic 25129 quart1lem 25137 atantayl2 25220 log2cnv 25227 log2ublem2 25230 log2ub 25232 gam1 25347 chtub 25493 bclbnd 25561 bposlem8 25572 lgsdir2lem1 25606 lgsdir2lem5 25610 2lgsoddprmlem3d 25694 ex-bc 28012 ex-gcd 28017 ipidsq 28267 ip1ilem 28383 ipdirilem 28386 ipasslem10 28396 siilem1 28408 hvmul2negi 28607 hvadd12i 28616 hvnegdii 28621 normlem1 28669 normlem9 28677 normsubi 28700 normpar2i 28715 polid2i 28716 chjassi 29047 chj12i 29083 pjoml2i 29146 hoadd12i 29338 lnophmlem2 29578 nmopcoadj2i 29663 indifundif 30062 aciunf1 30173 partfun 30186 ffsrn 30220 dpmul10 30320 dpmul1000 30324 dpadd2 30335 dpadd 30336 dpmul 30338 archirngz 30484 sqsscirc1 30795 sigaclfu2 31025 eulerpartlemd 31269 coinflippvt 31388 ballotth 31441 hgt750lem 31570 hgt750lem2 31571 quad3 32433 onint1 33317 bj-csbsn 33713 cnambfre 34381 sqmid3api 38601 rabren3dioph 38808 arearect 39218 areaquad 39219 resnonrel 39314 cononrel1 39316 cononrel2 39317 lhe4.4ex1a 40077 expgrowthi 40081 expgrowth 40083 binomcxplemnotnn0 40104 liminf0 41506 dvcosre 41627 stoweidlem34 41751 fouriersw 41948 |
Copyright terms: Public domain | W3C validator |