![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > opeq1d | GIF version |
Description: Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.) |
Ref | Expression |
---|---|
opeq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
opeq1d | ⊢ (𝜑 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opeq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | opeq1 3578 | . 2 ⊢ (𝐴 = 𝐵 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1285 〈cop 3409 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2064 |
This theorem depends on definitions: df-bi 115 df-3an 922 df-tru 1288 df-nf 1391 df-sb 1687 df-clab 2069 df-cleq 2075 df-clel 2078 df-nfc 2209 df-v 2604 df-un 2978 df-sn 3412 df-pr 3413 df-op 3415 |
This theorem is referenced by: oteq1 3587 oteq2 3588 opth 4000 cbvoprab2 5608 dfplpq2 6606 ltexnqq 6660 nnanq0 6710 addpinq1 6716 prarloclemlo 6746 prarloclem3 6749 prarloclem5 6752 prsrriota 7026 caucvgsrlemfv 7029 caucvgsr 7040 pitonnlem2 7077 pitonn 7078 recidpirq 7088 ax1rid 7105 axrnegex 7107 nntopi 7122 axcaucvglemval 7125 fseq1m1p1 9188 frecuzrdglem 9493 frecuzrdgg 9498 frecuzrdgdomlem 9499 frecuzrdgfunlem 9501 frecuzrdgsuctlem 9505 |
Copyright terms: Public domain | W3C validator |