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 4090 | . 2 ⊢ (𝐴 = 𝐵 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1483 ifcif 4086 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rab 2921 df-v 3202 df-un 3579 df-if 4087 |
This theorem is referenced by: ifeq12d 4106 ifbieq1d 4109 ifeq1da 4116 rabsnif 4258 fsuppmptif 8305 cantnflem1 8586 sumeq2w 14422 cbvsum 14425 isumless 14577 prodss 14677 subgmulg 17608 evlslem2 19512 dmatcrng 20308 scmatscmiddistr 20314 scmatcrng 20327 marrepfval 20366 mdetr0 20411 mdetunilem8 20425 madufval 20443 madugsum 20449 minmar1fval 20452 decpmatid 20575 monmatcollpw 20584 pmatcollpwscmatlem1 20594 cnmpt2pc 22727 pcoval2 22816 pcopt 22822 itgz 23547 iblss2 23572 itgss 23578 itgcn 23609 plyeq0lem 23966 dgrcolem2 24030 plydivlem4 24051 leibpi 24669 chtublem 24936 sumdchr 24997 bposlem6 25014 lgsval 25026 dchrvmasumiflem2 25191 padicabvcxp 25321 dfrdg3 31702 matunitlindflem1 33405 ftc1anclem2 33486 ftc1anclem5 33489 ftc1anclem7 33491 hoidifhspval 40822 hoimbl 40845 |
Copyright terms: Public domain | W3C validator |