![]() |
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 5715 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) | |
4 | 1, 2, 3 | mp2an 420 | 1 ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐷) |
Colors of variables: wff set class |
Syntax hints: = wceq 1299 (class class class)co 5706 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 |
This theorem depends on definitions: df-bi 116 df-3an 932 df-tru 1302 df-nf 1405 df-sb 1704 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-rex 2381 df-v 2643 df-un 3025 df-sn 3480 df-pr 3481 df-op 3483 df-uni 3684 df-br 3876 df-iota 5024 df-fv 5067 df-ov 5709 |
This theorem is referenced by: oveq123i 5720 1lt2nq 7115 halfnqq 7119 caucvgprprlemnbj 7402 caucvgprprlemaddq 7417 m1p1sr 7456 m1m1sr 7457 axi2m1 7560 negdii 7917 3t3e9 8729 8th4div3 8791 halfpm6th 8792 numma 9077 decmul10add 9102 4t3lem 9130 9t11e99 9163 sqdivapi 10217 sq4e2t8 10231 i4 10236 binom2i 10242 facp1 10317 fac2 10318 fac3 10319 fac4 10320 4bc2eq6 10361 cji 10515 fsumadd 11014 fsumsplitf 11016 fsumsplitsnun 11027 0.999... 11129 ef01bndlem 11261 cos2bnd 11265 3dvds2dec 11358 flodddiv4 11426 nn0gcdsq 11670 cnmpt2res 12247 ex-exp 12542 ex-fac 12543 ex-bc 12544 |
Copyright terms: Public domain | W3C validator |