![]() |
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 4550 | . 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
3 | iffalse 4540 | . . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = 𝐶) | |
4 | iffalse 4540 | . . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐵, 𝐶) = 𝐶) | |
5 | 3, 4 | eqtr4d 2778 | . . 3 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
6 | 5 | adantl 481 | . 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
7 | 2, 6 | pm2.61dan 813 | 1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 = wceq 1537 ifcif 4531 |
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 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-rab 3434 df-v 3480 df-un 3968 df-if 4532 |
This theorem is referenced by: ifeq12da 4564 cantnflem1d 9726 cantnflem1 9727 dfac12lem1 10182 xrmaxeq 13218 xrmineq 13219 rexmul 13310 max0add 15346 sumeq2ii 15726 fsumser 15763 ramcl 17063 dmdprdsplitlem 20072 coe1pwmul 22298 scmatscmiddistr 22530 mulmarep1gsum1 22595 maducoeval2 22662 madugsum 22665 madurid 22666 ptcld 23637 ibllem 25814 itgvallem3 25836 iblposlem 25842 iblss2 25856 iblmulc2 25881 cnplimc 25937 limcco 25943 dvexp3 26031 dchrinvcl 27312 lgsval2lem 27366 lgsval4lem 27367 lgsneg 27380 lgsmod 27382 lgsdilem2 27392 rpvmasum2 27571 mrsubrn 35498 ftc1anclem6 37685 ftc1anclem8 37687 fsuppind 42577 |
Copyright terms: Public domain | W3C validator |