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 5751 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) | |
4 | 1, 2, 3 | mp2an 422 | 1 ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐷) |
Colors of variables: wff set class |
Syntax hints: = wceq 1316 (class class class)co 5742 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 683 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-10 1468 ax-11 1469 ax-i12 1470 ax-bndl 1471 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-3an 949 df-tru 1319 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-nfc 2247 df-rex 2399 df-v 2662 df-un 3045 df-sn 3503 df-pr 3504 df-op 3506 df-uni 3707 df-br 3900 df-iota 5058 df-fv 5101 df-ov 5745 |
This theorem is referenced by: oveq123i 5756 1lt2nq 7182 halfnqq 7186 caucvgprprlemnbj 7469 caucvgprprlemaddq 7484 m1p1sr 7536 m1m1sr 7537 axi2m1 7651 negdii 8014 3t3e9 8845 8th4div3 8907 halfpm6th 8908 numma 9193 decmul10add 9218 4t3lem 9246 9t11e99 9279 halfthird 9292 5recm6rec 9293 sqdivapi 10344 sq4e2t8 10358 i4 10363 binom2i 10369 facp1 10444 fac2 10445 fac3 10446 fac4 10447 4bc2eq6 10488 cji 10642 fsumadd 11143 fsumsplitf 11145 fsumsplitsnun 11156 0.999... 11258 ef01bndlem 11390 cos2bnd 11394 3dvds2dec 11490 flodddiv4 11558 nn0gcdsq 11805 cnmpt2res 12393 txmetcnp 12614 dveflem 12782 efhalfpi 12807 efipi 12809 sin2pi 12811 ef2pi 12813 sincosq3sgn 12836 sincosq4sgn 12837 sinq34lt0t 12839 sincos4thpi 12848 tan4thpi 12849 sincos6thpi 12850 sincos3rdpi 12851 pigt3 12852 ex-exp 12866 ex-fac 12867 ex-bc 12868 |
Copyright terms: Public domain | W3C validator |