![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ifeq1da | Structured version Visualization version GIF version |
Description: Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Ref | Expression |
---|---|
ifeq1da.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
ifeq1da | ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ifeq1da.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐵) | |
2 | 1 | ifeq1d 4137 | . 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
3 | iffalse 4128 | . . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = 𝐶) | |
4 | iffalse 4128 | . . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐵, 𝐶) = 𝐶) | |
5 | 3, 4 | eqtr4d 2688 | . . 3 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
6 | 5 | adantl 481 | . 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
7 | 2, 6 | pm2.61dan 849 | 1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 383 = wceq 1523 ifcif 4119 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-rab 2950 df-v 3233 df-un 3612 df-if 4120 |
This theorem is referenced by: ifeq12da 4151 cantnflem1d 8623 cantnflem1 8624 dfac12lem1 9003 xrmaxeq 12048 xrmineq 12049 rexmul 12139 max0add 14094 sumeq2ii 14467 fsumser 14505 ramcl 15780 dmdprdsplitlem 18482 coe1pwmul 19697 scmatscmiddistr 20362 mulmarep1gsum1 20427 maducoeval2 20494 madugsum 20497 madurid 20498 ptcld 21464 copco 22864 ibllem 23576 itgvallem3 23597 iblposlem 23603 iblss2 23617 iblmulc2 23642 cnplimc 23696 limcco 23702 dvexp3 23786 dchrinvcl 25023 lgsval2lem 25077 lgsval4lem 25078 lgsneg 25091 lgsmod 25093 lgsdilem2 25103 rpvmasum2 25246 mrsubrn 31536 ftc1anclem6 33620 ftc1anclem8 33622 |
Copyright terms: Public domain | W3C validator |