![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > oveqd | GIF version |
Description: Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.) |
Ref | Expression |
---|---|
oveq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
oveqd | ⊢ (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | oveq 5880 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷)) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1353 (class class class)co 5874 |
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 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-rex 2461 df-uni 3810 df-br 4004 df-iota 5178 df-fv 5224 df-ov 5877 |
This theorem is referenced by: oveq123d 5895 oveqdr 5902 csbov12g 5913 ovmpodxf 5999 oprssov 6015 ofeq 6084 fnmpoovd 6215 seqeq2 10446 imasex 12708 imasival 12709 plusffvalg 12735 mgm1 12743 grpidvalg 12746 grpidd 12756 sgrp1 12770 ismndd 12792 issubmnd 12797 mnd1 12801 ismhm 12807 issubm 12817 isgrp 12837 isgrpd2e 12850 grpidd2 12868 grpinvfvalg 12869 grp1 12930 subg0 12993 subginv 12994 subgcl 12997 issubgrpd2 13003 isnsg 13015 nmznsg 13026 iscmn 13049 iscmnd 13054 dfur2g 13098 issrg 13101 srgcl 13106 srgass 13107 srgideu 13108 issrgid 13117 srgpcomp 13126 srgpcompp 13127 isring 13136 ringcl 13149 crngcom 13150 iscrng2 13151 ringass 13152 ringideu 13153 isringid 13161 ringidss 13165 ringpropd 13170 ring1 13189 opprmulg 13196 oppr0g 13204 oppr1g 13205 opprnegg 13206 mulgass3 13207 reldvdsrsrg 13214 dvdsrvald 13215 dvdsrd 13216 opprunitd 13232 dvrvald 13256 rdivmuldivd 13266 islring 13286 lringuplu 13290 aprval 13293 aprap 13297 subrg1 13312 subrgmcl 13314 subrgdvds 13316 subrguss 13317 subrginv 13318 subrgdv 13319 subrgunit 13320 subrgugrp 13321 issubrg3 13328 blfvalps 13778 |
Copyright terms: Public domain | W3C validator |