![]() |
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 4443 | . 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
3 | iffalse 4434 | . . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = 𝐶) | |
4 | iffalse 4434 | . . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐵, 𝐶) = 𝐶) | |
5 | 3, 4 | eqtr4d 2836 | . . 3 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
6 | 5 | adantl 485 | . 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
7 | 2, 6 | pm2.61dan 812 | 1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 399 = wceq 1538 ifcif 4425 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-12 2175 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-rab 3115 df-v 3443 df-un 3886 df-if 4426 |
This theorem is referenced by: ifeq12da 4457 cantnflem1d 9135 cantnflem1 9136 dfac12lem1 9554 xrmaxeq 12560 xrmineq 12561 rexmul 12652 max0add 14662 sumeq2ii 15042 fsumser 15079 ramcl 16355 dmdprdsplitlem 19152 coe1pwmul 20908 scmatscmiddistr 21113 mulmarep1gsum1 21178 maducoeval2 21245 madugsum 21248 madurid 21249 ptcld 22218 ibllem 24368 itgvallem3 24389 iblposlem 24395 iblss2 24409 iblmulc2 24434 cnplimc 24490 limcco 24496 dvexp3 24581 dchrinvcl 25837 lgsval2lem 25891 lgsval4lem 25892 lgsneg 25905 lgsmod 25907 lgsdilem2 25917 rpvmasum2 26096 mrsubrn 32873 ftc1anclem6 35135 ftc1anclem8 35137 fsuppind 39456 |
Copyright terms: Public domain | W3C validator |