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 5845 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) | |
4 | 1, 2, 3 | mp2an 423 | 1 ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐷) |
Colors of variables: wff set class |
Syntax hints: = wceq 1342 (class class class)co 5836 |
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 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-3an 969 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-rex 2448 df-v 2723 df-un 3115 df-sn 3576 df-pr 3577 df-op 3579 df-uni 3784 df-br 3977 df-iota 5147 df-fv 5190 df-ov 5839 |
This theorem is referenced by: oveq123i 5850 1lt2nq 7338 halfnqq 7342 caucvgprprlemnbj 7625 caucvgprprlemaddq 7640 m1p1sr 7692 m1m1sr 7693 axi2m1 7807 negdii 8173 3t3e9 9005 8th4div3 9067 halfpm6th 9068 numma 9356 decmul10add 9381 4t3lem 9409 9t11e99 9442 halfthird 9455 5recm6rec 9456 fz0to3un2pr 10048 sqdivapi 10528 sq4e2t8 10542 i4 10547 binom2i 10553 facp1 10632 fac2 10633 fac3 10634 fac4 10635 4bc2eq6 10676 cji 10830 fsumadd 11333 fsumsplitf 11335 fsumsplitsnun 11346 0.999... 11448 fprodmul 11518 fprodsplitf 11559 ef01bndlem 11683 cos2bnd 11687 3dvds2dec 11788 flodddiv4 11856 nn0gcdsq 12109 pythagtriplem16 12188 cnmpt2res 12838 txmetcnp 13059 dveflem 13228 efhalfpi 13261 efipi 13263 sin2pi 13265 ef2pi 13267 sincosq3sgn 13290 sincosq4sgn 13291 sinq34lt0t 13293 sincos4thpi 13302 tan4thpi 13303 sincos6thpi 13304 sincos3rdpi 13305 pigt3 13306 ex-exp 13445 ex-fac 13446 ex-bc 13447 |
Copyright terms: Public domain | W3C validator |