![]() |
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 4537 | . 2 ⊢ (𝐴 = 𝐵 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1534 ifcif 4533 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3420 df-v 3464 df-un 3952 df-if 4534 |
This theorem is referenced by: ifeq12d 4554 ifbieq1d 4557 ifeq1da 4564 rabsnif 4732 fsuppmptif 9442 cantnflem1 9732 sumeq2w 15696 cbvsum 15699 isumless 15849 prodss 15949 subgmulg 19134 evlslem2 22094 selvval 22130 dmatcrng 22495 scmatscmiddistr 22501 scmatcrng 22514 marrepfval 22553 mdetr0 22598 mdetunilem8 22612 madufval 22630 madugsum 22636 minmar1fval 22639 decpmatid 22763 monmatcollpw 22772 pmatcollpwscmatlem1 22782 cnmpopc 24940 pcoval2 25034 pcopt 25040 itgz 25801 iblss2 25826 itgss 25832 itgcn 25865 plyeq0lem 26237 dgrcolem2 26302 plydivlem4 26324 leibpi 26970 chtublem 27240 sumdchr 27301 bposlem6 27318 lgsval 27330 dchrvmasumiflem2 27531 padicabvcxp 27661 dfrdg3 35620 matunitlindflem1 37317 ftc1anclem2 37395 ftc1anclem5 37398 ftc1anclem7 37400 fsuppssindlem2 42064 fsuppssind 42065 mnringmulrvald 43901 hoidifhspval 46229 hoimbl 46252 |
Copyright terms: Public domain | W3C validator |