![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > tpeq123d | Structured version Visualization version GIF version |
Description: Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.) |
Ref | Expression |
---|---|
tpeq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
tpeq123d.2 | ⊢ (𝜑 → 𝐶 = 𝐷) |
tpeq123d.3 | ⊢ (𝜑 → 𝐸 = 𝐹) |
Ref | Expression |
---|---|
tpeq123d | ⊢ (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐹}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tpeq1d.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | 1 | tpeq1d 4742 | . 2 ⊢ (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐶, 𝐸}) |
3 | tpeq123d.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
4 | 3 | tpeq2d 4743 | . 2 ⊢ (𝜑 → {𝐵, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐸}) |
5 | tpeq123d.3 | . . 3 ⊢ (𝜑 → 𝐸 = 𝐹) | |
6 | 5 | tpeq3d 4744 | . 2 ⊢ (𝜑 → {𝐵, 𝐷, 𝐸} = {𝐵, 𝐷, 𝐹}) |
7 | 2, 4, 6 | 3eqtrd 2775 | 1 ⊢ (𝜑 → {𝐴, 𝐶, 𝐸} = {𝐵, 𝐷, 𝐹}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 {ctp 4626 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-v 3475 df-un 3949 df-sn 4623 df-pr 4625 df-tp 4627 |
This theorem is referenced by: fz0tp 13584 fz0to4untppr 13586 fzo0to3tp 13700 fzo1to4tp 13702 prdsval 17383 imasval 17439 fucval 17892 fucpropd 17912 setcval 18009 catcval 18032 estrcval 18057 xpcval 18111 efmnd 18726 psrval 21399 om1val 24475 s3rn 31983 idlsrgval 32460 ldualset 37798 erngfset 39473 erngfset-rN 39481 dvafset 39678 dvaset 39679 dvhfset 39754 dvhset 39755 hlhilset 40608 rabren3dioph 41322 mendval 41694 oaun3 41901 nnsum4primesodd 46234 nnsum4primesoddALTV 46235 rngcvalALTV 46505 ringcvalALTV 46551 mndtcval 47351 |
Copyright terms: Public domain | W3C validator |