![]() |
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 4226 | . 2 ⊢ (𝐴 = 𝐵 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1624 ifcif 4222 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1627 df-ex 1846 df-nf 1851 df-sb 2039 df-clab 2739 df-cleq 2745 df-clel 2748 df-nfc 2883 df-rab 3051 df-v 3334 df-un 3712 df-if 4223 |
This theorem is referenced by: ifeq12d 4242 ifbieq1d 4245 ifeq1da 4252 rabsnif 4394 fsuppmptif 8462 cantnflem1 8751 sumeq2w 14613 cbvsum 14616 isumless 14768 prodss 14868 subgmulg 17801 evlslem2 19706 dmatcrng 20502 scmatscmiddistr 20508 scmatcrng 20521 marrepfval 20560 mdetr0 20605 mdetunilem8 20619 madufval 20637 madugsum 20643 minmar1fval 20646 decpmatid 20769 monmatcollpw 20778 pmatcollpwscmatlem1 20788 cnmpt2pc 22920 pcoval2 23008 pcopt 23014 itgz 23738 iblss2 23763 itgss 23769 itgcn 23800 plyeq0lem 24157 dgrcolem2 24221 plydivlem4 24242 leibpi 24860 chtublem 25127 sumdchr 25188 bposlem6 25205 lgsval 25217 dchrvmasumiflem2 25382 padicabvcxp 25512 dfrdg3 31999 matunitlindflem1 33710 ftc1anclem2 33791 ftc1anclem5 33794 ftc1anclem7 33796 hoidifhspval 41320 hoimbl 41343 |
Copyright terms: Public domain | W3C validator |