![]() |
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 4506 | . 2 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
3 | ifeq12d.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
4 | 3 | ifeq2d 4507 | . 2 ⊢ (𝜑 → if(𝜓, 𝐵, 𝐶) = if(𝜓, 𝐵, 𝐷)) |
5 | 2, 4 | eqtrd 2777 | 1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ifcif 4487 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-rab 3409 df-v 3448 df-un 3916 df-if 4488 |
This theorem is referenced by: ifbieq12d 4515 csbif 4544 oev 8461 dfac12r 10083 xaddpnf1 13146 swrdccat3blem 14628 relexpsucnnr 14911 ruclem1 16114 eucalgval 16459 gsumpropd 18534 gsumpropd2lem 18535 gsumress 18538 mulgfval 18875 mulgfvalALT 18876 mulgpropd 18919 frgpup3lem 19560 isobs 21129 uvcfval 21193 subrgmvr 21437 matsc 21802 scmatscmide 21859 marrepval0 21913 marepvval0 21918 mulmarep1el 21924 madufval 21989 madugsum 21995 minmar1fval 21998 pmat1opsc 22051 pmat1ovscd 22052 mat2pmat1 22084 decpmatid 22122 idpm2idmp 22153 pcoval 24377 pcorevlem 24392 itg2const 25108 ditgeq3 25217 efrlim 26322 lgsval 26652 rpvmasum2 26863 fzto1st 31955 psgnfzto1st 31957 xrhval 32602 itg2addnclem 36132 ftc1anclem5 36158 hdmap1fval 40262 sticksstones12a 40568 sticksstones12 40569 rhmmpl 40744 fsuppind 40768 mhphf 40774 dgrsub2 41465 reabssgn 41915 dirkerval 44339 fourierdlem111 44465 fourierdlem112 44466 fourierdlem113 44467 hsphoif 44824 hsphoival 44827 hoidmvlelem5 44847 hoidifhspval2 44863 hspmbllem2 44875 itcoval 46754 |
Copyright terms: Public domain | W3C validator |