|   | 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 4545 | . 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶)) | 
| 3 | iffalse 4534 | . . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐶) = 𝐶) | |
| 4 | iffalse 4534 | . . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐵, 𝐶) = 𝐶) | |
| 5 | 3, 4 | eqtr4d 2780 | . . 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 1540 ifcif 4525 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-un 3956 df-if 4526 | 
| This theorem is referenced by: ifeq12da 4559 cantnflem1d 9728 cantnflem1 9729 dfac12lem1 10184 xrmaxeq 13221 xrmineq 13222 rexmul 13313 max0add 15349 sumeq2ii 15729 fsumser 15766 ramcl 17067 dmdprdsplitlem 20057 coe1pwmul 22282 scmatscmiddistr 22514 mulmarep1gsum1 22579 maducoeval2 22646 madugsum 22649 madurid 22650 ptcld 23621 ibllem 25799 itgvallem3 25821 iblposlem 25827 iblss2 25841 iblmulc2 25866 cnplimc 25922 limcco 25928 dvexp3 26016 dchrinvcl 27297 lgsval2lem 27351 lgsval4lem 27352 lgsneg 27365 lgsmod 27367 lgsdilem2 27377 rpvmasum2 27556 mrsubrn 35518 ftc1anclem6 37705 ftc1anclem8 37707 fsuppind 42600 | 
| Copyright terms: Public domain | W3C validator |