![]() |
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 4246 | . 2 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
3 | ifeq12d.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
4 | 3 | ifeq2d 4247 | . 2 ⊢ (𝜑 → if(𝜓, 𝐵, 𝐶) = if(𝜓, 𝐵, 𝐷)) |
5 | 2, 4 | eqtrd 2792 | 1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1630 ifcif 4228 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1986 ax-6 2052 ax-7 2088 ax-9 2146 ax-10 2166 ax-11 2181 ax-12 2194 ax-13 2389 ax-ext 2738 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2045 df-clab 2745 df-cleq 2751 df-clel 2754 df-nfc 2889 df-rab 3057 df-v 3340 df-un 3718 df-if 4229 |
This theorem is referenced by: ifbieq12d 4255 csbif 4280 oev 7761 dfac12r 9158 xaddpnf1 12248 swrdccat3blem 13693 relexpsucnnr 13962 ruclem1 15157 eucalgval 15495 gsumpropd 17471 gsumpropd2lem 17472 gsumress 17475 mulgfval 17741 mulgpropd 17783 frgpup3lem 18388 subrgmvr 19661 isobs 20264 uvcfval 20323 matsc 20456 scmatscmide 20513 marrepval0 20567 marepvval0 20572 mulmarep1el 20578 madufval 20643 madugsum 20649 minmar1fval 20652 pmat1opsc 20704 pmat1ovscd 20705 mat2pmat1 20737 decpmatid 20775 idpm2idmp 20806 pcoval 23009 pcorevlem 23024 itg2const 23704 ditgeq3 23811 efrlim 24893 lgsval 25223 rpvmasum2 25398 fzto1st 30160 psgnfzto1st 30162 xrhval 30369 itg2addnclem 33772 ftc1anclem5 33800 hdmap1fval 37586 dgrsub2 38205 dirkerval 40809 fourierdlem111 40935 fourierdlem112 40936 fourierdlem113 40937 hsphoif 41294 hsphoival 41297 hoidmvlelem5 41317 hoidifhspval2 41333 hspmbllem2 41345 |
Copyright terms: Public domain | W3C validator |