Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ifeq1d | Structured version Visualization version GIF version |
Description: Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.) |
Ref | Expression |
---|---|
ifeq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
ifeq1d | ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ifeq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | ifeq1 4471 | . 2 ⊢ (𝐴 = 𝐵 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ifcif 4467 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3496 df-un 3941 df-if 4468 |
This theorem is referenced by: ifeq12d 4487 ifbieq1d 4490 ifeq1da 4497 rabsnif 4659 fsuppmptif 8863 cantnflem1 9152 sumeq2w 15049 cbvsum 15052 isumless 15200 prodss 15301 subgmulg 18293 evlslem2 20292 selvval 20331 dmatcrng 21111 scmatscmiddistr 21117 scmatcrng 21130 marrepfval 21169 mdetr0 21214 mdetunilem8 21228 madufval 21246 madugsum 21252 minmar1fval 21255 decpmatid 21378 monmatcollpw 21387 pmatcollpwscmatlem1 21397 cnmpopc 23532 pcoval2 23620 pcopt 23626 itgz 24381 iblss2 24406 itgss 24412 itgcn 24443 plyeq0lem 24800 dgrcolem2 24864 plydivlem4 24885 leibpi 25520 chtublem 25787 sumdchr 25848 bposlem6 25865 lgsval 25877 dchrvmasumiflem2 26078 padicabvcxp 26208 dfrdg3 33041 matunitlindflem1 34903 ftc1anclem2 34983 ftc1anclem5 34986 ftc1anclem7 34988 hoidifhspval 42910 hoimbl 42933 |
Copyright terms: Public domain | W3C validator |