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 5843 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶)) | |
2 | oveq2 5844 | . 2 ⊢ (𝐶 = 𝐷 → (𝐵𝐹𝐶) = (𝐵𝐹𝐷)) | |
3 | 1, 2 | sylan9eq 2217 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 = 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: oveq12i 5848 oveq12d 5854 oveqan12d 5855 ecopoveq 6587 ecopovtrn 6589 ecopovtrng 6592 th3qlem1 6594 th3qlem2 6595 mulcmpblnq 7300 addpipqqs 7302 ordpipqqs 7306 enq0breq 7368 mulcmpblnq0 7376 nqpnq0nq 7385 nqnq0a 7386 nqnq0m 7387 nq0m0r 7388 nq0a0 7389 distrlem5prl 7518 distrlem5pru 7519 addcmpblnr 7671 ltsrprg 7679 mulgt0sr 7710 add20 8363 cru 8491 qaddcl 9564 qmulcl 9566 xaddval 9772 xnn0xadd0 9794 fzopth 9986 modqval 10249 seqvalcd 10384 seqovcd 10388 1exp 10474 m1expeven 10492 nn0opthd 10624 faclbnd 10643 faclbnd3 10645 bcn0 10657 reval 10777 absval 10929 clim 11208 fsumparts 11397 dvds2add 11751 dvds2sub 11752 opoe 11817 omoe 11818 opeo 11819 omeo 11820 gcddvds 11881 gcdcl 11884 gcdeq0 11895 gcdneg 11900 gcdaddm 11902 gcdabs 11906 gcddiv 11937 eucalgval2 11964 lcmabs 11987 rpmul 12009 divgcdcoprmex 12013 prmexpb 12062 rpexp 12064 nn0gcdsq 12111 pcqmul 12214 cnmpt2t 12840 cnmpt22f 12842 hmeofvalg 12850 bdmetval 13047 |
Copyright terms: Public domain | W3C validator |