![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > oveq12i | GIF version |
Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Ref | Expression |
---|---|
oveq1i.1 | ⊢ 𝐴 = 𝐵 |
oveq12i.2 | ⊢ 𝐶 = 𝐷 |
Ref | Expression |
---|---|
oveq12i | ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | oveq12i.2 | . 2 ⊢ 𝐶 = 𝐷 | |
3 | oveq12 5552 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) | |
4 | 1, 2, 3 | mp2an 417 | 1 ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐷) |
Colors of variables: wff set class |
Syntax hints: = wceq 1285 (class class class)co 5543 |
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-rex 2355 df-v 2604 df-un 2978 df-sn 3412 df-pr 3413 df-op 3415 df-uni 3610 df-br 3794 df-iota 4897 df-fv 4940 df-ov 5546 |
This theorem is referenced by: oveq123i 5557 1lt2nq 6658 halfnqq 6662 caucvgprprlemnbj 6945 caucvgprprlemaddq 6960 m1p1sr 6999 m1m1sr 7000 axi2m1 7103 negdii 7459 3t3e9 8256 8th4div3 8317 halfpm6th 8318 numma 8601 decmul10add 8626 4t3lem 8654 9t11e99 8687 sqdivapi 9656 i4 9674 binom2i 9680 facp1 9754 fac2 9755 fac3 9756 fac4 9757 4bc2eq6 9798 cji 9927 3dvds2dec 10410 flodddiv4 10478 ex-fac 10716 ex-bc 10717 |
Copyright terms: Public domain | W3C validator |