![]() |
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 4310 | . 2 ⊢ (𝐴 = 𝐵 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1658 ifcif 4306 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-rab 3126 df-v 3416 df-un 3803 df-if 4307 |
This theorem is referenced by: ifeq12d 4326 ifbieq1d 4329 ifeq1da 4336 rabsnif 4476 fsuppmptif 8574 cantnflem1 8863 sumeq2w 14799 cbvsum 14802 isumless 14951 prodss 15050 subgmulg 17959 evlslem2 19872 dmatcrng 20676 scmatscmiddistr 20682 scmatcrng 20695 marrepfval 20734 mdetr0 20779 mdetunilem8 20793 madufval 20811 madugsum 20817 minmar1fval 20820 decpmatid 20945 monmatcollpw 20954 pmatcollpwscmatlem1 20964 cnmpt2pc 23097 pcoval2 23185 pcopt 23191 itgz 23946 iblss2 23971 itgss 23977 itgcn 24008 plyeq0lem 24365 dgrcolem2 24429 plydivlem4 24450 leibpi 25082 chtublem 25349 sumdchr 25410 bposlem6 25427 lgsval 25439 dchrvmasumiflem2 25604 padicabvcxp 25734 dfrdg3 32240 matunitlindflem1 33949 ftc1anclem2 34029 ftc1anclem5 34032 ftc1anclem7 34034 hoidifhspval 41616 hoimbl 41639 |
Copyright terms: Public domain | W3C validator |