![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ifeq12d | Structured version Visualization version GIF version |
Description: Equality deduction for conditional operator. (Contributed by NM, 24-Mar-2015.) |
Ref | Expression |
---|---|
ifeq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
ifeq12d.2 | ⊢ (𝜑 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
ifeq12d | ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ifeq1d.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | 1 | ifeq1d 4547 | . 2 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
3 | ifeq12d.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
4 | 3 | ifeq2d 4548 | . 2 ⊢ (𝜑 → if(𝜓, 𝐵, 𝐶) = if(𝜓, 𝐵, 𝐷)) |
5 | 2, 4 | eqtrd 2771 | 1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1540 ifcif 4528 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-tru 1543 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-rab 3432 df-v 3475 df-un 3953 df-if 4529 |
This theorem is referenced by: ifbieq12d 4556 csbif 4585 oev 8520 dfac12r 10147 xaddpnf1 13212 swrdccat3blem 14696 relexpsucnnr 14979 ruclem1 16181 eucalgval 16526 gsumpropd 18609 gsumpropd2lem 18610 gsumress 18613 mulgfval 18995 mulgfvalALT 18996 mulgpropd 19039 frgpup3lem 19693 isobs 21585 uvcfval 21649 subrgmvr 21899 matsc 22272 scmatscmide 22329 marrepval0 22383 marepvval0 22388 mulmarep1el 22394 madufval 22459 madugsum 22465 minmar1fval 22468 pmat1opsc 22521 pmat1ovscd 22522 mat2pmat1 22554 decpmatid 22592 idpm2idmp 22623 pcoval 24858 pcorevlem 24873 itg2const 25590 ditgeq3 25699 efrlim 26815 lgsval 27147 rpvmasum2 27358 fzto1st 32698 psgnfzto1st 32700 xrhval 33462 itg2addnclem 37003 ftc1anclem5 37029 hdmap1fval 41131 sticksstones12a 41440 sticksstones12 41441 rhmmpl 41588 selvvvval 41620 fsuppind 41625 dgrsub2 42340 reabssgn 42850 dirkerval 45266 fourierdlem111 45392 fourierdlem112 45393 fourierdlem113 45394 hsphoif 45751 hsphoival 45754 hoidmvlelem5 45774 hoidifhspval2 45790 hspmbllem2 45802 itcoval 47509 |
Copyright terms: Public domain | W3C validator |