![]() |
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 5909 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) | |
4 | 1, 2, 3 | mp2an 426 | 1 ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐷) |
Colors of variables: wff set class |
Syntax hints: = wceq 1364 (class class class)co 5900 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-rex 2474 df-v 2754 df-un 3148 df-sn 3616 df-pr 3617 df-op 3619 df-uni 3828 df-br 4022 df-iota 5199 df-fv 5246 df-ov 5903 |
This theorem is referenced by: oveq123i 5914 1lt2nq 7440 halfnqq 7444 caucvgprprlemnbj 7727 caucvgprprlemaddq 7742 m1p1sr 7794 m1m1sr 7795 axi2m1 7909 negdii 8276 3t3e9 9111 8th4div3 9173 halfpm6th 9174 numma 9462 decmul10add 9487 4t3lem 9515 9t11e99 9548 halfthird 9561 5recm6rec 9562 fz0to3un2pr 10159 sqdivapi 10644 sq4e2t8 10658 i4 10663 binom2i 10669 facp1 10751 fac2 10752 fac3 10753 fac4 10754 4bc2eq6 10795 cji 10952 fsumadd 11455 fsumsplitf 11457 fsumsplitsnun 11468 0.999... 11570 fprodmul 11640 fprodsplitf 11681 ef01bndlem 11805 cos2bnd 11809 3dvds2dec 11912 flodddiv4 11980 nn0gcdsq 12243 pythagtriplem16 12322 4sqlem19 12452 ecqusaddd 13202 isrhm 13533 cnmpt2res 14282 txmetcnp 14503 dveflem 14672 efhalfpi 14705 efipi 14707 sin2pi 14709 ef2pi 14711 sincosq3sgn 14734 sincosq4sgn 14735 sinq34lt0t 14737 sincos4thpi 14746 tan4thpi 14747 sincos6thpi 14748 sincos3rdpi 14749 pigt3 14750 lgsdi 14924 2lgsoddprmlem3c 14943 2lgsoddprmlem3d 14944 ex-exp 14965 ex-fac 14966 ex-bc 14967 |
Copyright terms: Public domain | W3C validator |