Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > oveq12 | GIF version |
Description: Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.) |
Ref | Expression |
---|---|
oveq12 | ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq1 5539 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶)) | |
2 | oveq2 5540 | . 2 ⊢ (𝐶 = 𝐷 → (𝐵𝐹𝐶) = (𝐵𝐹𝐷)) | |
3 | 1, 2 | sylan9eq 2133 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 = wceq 1284 (class class class)co 5532 |
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 662 ax-5 1376 ax-7 1377 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-8 1435 ax-10 1436 ax-11 1437 ax-i12 1438 ax-bndl 1439 ax-4 1440 ax-17 1459 ax-i9 1463 ax-ial 1467 ax-i5r 1468 ax-ext 2063 |
This theorem depends on definitions: df-bi 115 df-3an 921 df-tru 1287 df-nf 1390 df-sb 1686 df-clab 2068 df-cleq 2074 df-clel 2077 df-nfc 2208 df-rex 2354 df-v 2603 df-un 2977 df-sn 3404 df-pr 3405 df-op 3407 df-uni 3602 df-br 3786 df-iota 4887 df-fv 4930 df-ov 5535 |
This theorem is referenced by: oveq12i 5544 oveq12d 5550 oveqan12d 5551 sprmpt2 5880 ecopoveq 6224 ecopovtrn 6226 ecopovtrng 6229 th3qlem1 6231 th3qlem2 6232 mulcmpblnq 6558 addpipqqs 6560 ordpipqqs 6564 enq0breq 6626 mulcmpblnq0 6634 nqpnq0nq 6643 nqnq0a 6644 nqnq0m 6645 nq0m0r 6646 nq0a0 6647 distrlem5prl 6776 distrlem5pru 6777 addcmpblnr 6916 ltsrprg 6924 mulgt0sr 6954 add20 7578 cru 7702 qaddcl 8720 qmulcl 8722 fzopth 9079 modqval 9326 1exp 9505 m1expeven 9523 nn0opthd 9649 faclbnd 9668 faclbnd3 9670 bcn0 9682 reval 9736 absval 9887 clim 10120 dvds2add 10229 dvds2sub 10230 opoe 10295 omoe 10296 opeo 10297 omeo 10298 gcddvds 10355 gcdcl 10358 gcdeq0 10368 gcdneg 10373 gcdaddm 10375 gcdabs 10379 gcddiv 10408 eucalgval2 10435 lcmabs 10458 rpmul 10480 divgcdcoprmex 10484 prmexpb 10530 rpexp 10532 |
Copyright terms: Public domain | W3C validator |