| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > oteq3d | Structured version Visualization version GIF version | ||
| Description: Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.) |
| Ref | Expression |
|---|---|
| oteq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
| Ref | Expression |
|---|---|
| oteq3d | ⊢ (𝜑 → 〈𝐶, 𝐷, 𝐴〉 = 〈𝐶, 𝐷, 𝐵〉) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | oteq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
| 2 | oteq3 4853 | . 2 ⊢ (𝐴 = 𝐵 → 〈𝐶, 𝐷, 𝐴〉 = 〈𝐶, 𝐷, 𝐵〉) | |
| 3 | 1, 2 | syl 18 | 1 ⊢ (𝜑 → 〈𝐶, 𝐷, 𝐴〉 = 〈𝐶, 𝐷, 𝐵〉) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1567 〈cotp 4602 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-ext 2741 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-sb 2098 df-clab 2748 df-cleq 2761 df-clel 2844 df-rab 3424 df-v 3465 df-dif 3916 df-un 3918 df-ss 3930 df-nul 4295 df-if 4493 df-sn 4595 df-pr 4597 df-op 4601 df-ot 4603 |
| This theorem is referenced by: oteq123d 4857 idafval 18114 coafval 18121 arwlid 18129 arwrid 18130 arwass 18131 efgi 19789 efgtf 19792 efgtval 19793 efgval2 19794 mapdh6bN 42401 mapdh6cN 42402 mapdh6dN 42403 mapdh6gN 42406 hdmap1l6b 42475 hdmap1l6c 42476 hdmap1l6d 42477 hdmap1l6g 42480 |
| Copyright terms: Public domain | W3C validator |