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 4484 | . 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
3 | iffalse 4475 | . . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = 𝐶) | |
4 | iffalse 4475 | . . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐵, 𝐶) = 𝐶) | |
5 | 3, 4 | eqtr4d 2859 | . . 3 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
6 | 5 | adantl 484 | . 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
7 | 2, 6 | pm2.61dan 811 | 1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 398 = wceq 1533 ifcif 4466 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3496 df-un 3940 df-if 4467 |
This theorem is referenced by: ifeq12da 4498 cantnflem1d 9145 cantnflem1 9146 dfac12lem1 9563 xrmaxeq 12566 xrmineq 12567 rexmul 12658 max0add 14664 sumeq2ii 15044 fsumser 15081 ramcl 16359 dmdprdsplitlem 19153 coe1pwmul 20441 scmatscmiddistr 21111 mulmarep1gsum1 21176 maducoeval2 21243 madugsum 21246 madurid 21247 ptcld 22215 ibllem 24359 itgvallem3 24380 iblposlem 24386 iblss2 24400 iblmulc2 24425 cnplimc 24479 limcco 24485 dvexp3 24569 dchrinvcl 25823 lgsval2lem 25877 lgsval4lem 25878 lgsneg 25891 lgsmod 25893 lgsdilem2 25903 rpvmasum2 26082 mrsubrn 32755 ftc1anclem6 34966 ftc1anclem8 34968 |
Copyright terms: Public domain | W3C validator |