| 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 4529 | . 2 ⊢ (𝐴 = 𝐵 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ifcif 4525 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-un 3956 df-if 4526 |
| This theorem is referenced by: ifeq12d 4547 ifbieq1d 4550 ifeq1da 4557 rabsnif 4723 fsuppmptif 9439 cantnflem1 9729 sumeq2w 15728 cbvsum 15731 cbvsumv 15732 sumeq2sdv 15739 isumless 15881 prodeq2sdv 15959 prodss 15983 subgmulg 19158 evlslem2 22103 selvval 22139 dmatcrng 22508 scmatscmiddistr 22514 scmatcrng 22527 marrepfval 22566 mdetr0 22611 mdetunilem8 22625 madufval 22643 madugsum 22649 minmar1fval 22652 decpmatid 22776 monmatcollpw 22785 pmatcollpwscmatlem1 22795 cnmpopc 24955 pcoval2 25049 pcopt 25055 itgz 25816 iblss2 25841 itgss 25847 itgcn 25880 plyeq0lem 26249 dgrcolem2 26314 plydivlem4 26338 leibpi 26985 chtublem 27255 sumdchr 27316 bposlem6 27333 lgsval 27345 dchrvmasumiflem2 27546 padicabvcxp 27676 dfrdg3 35797 cbvsumdavw 36280 matunitlindflem1 37623 ftc1anclem2 37701 ftc1anclem5 37704 ftc1anclem7 37706 fsuppssindlem2 42602 fsuppssind 42603 mnringmulrvald 44246 hoidifhspval 46623 hoimbl 46646 |
| Copyright terms: Public domain | W3C validator |