|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > ifeq2da | Structured version Visualization version GIF version | ||
| Description: Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.) | 
| Ref | Expression | 
|---|---|
| ifeq2da.1 | ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐴 = 𝐵) | 
| Ref | Expression | 
|---|---|
| ifeq2da | ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | iftrue 4530 | . . . 4 ⊢ (𝜓 → if(𝜓, 𝐶, 𝐴) = 𝐶) | |
| 2 | iftrue 4530 | . . . 4 ⊢ (𝜓 → if(𝜓, 𝐶, 𝐵) = 𝐶) | |
| 3 | 1, 2 | eqtr4d 2779 | . . 3 ⊢ (𝜓 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) | 
| 4 | 3 | adantl 481 | . 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) | 
| 5 | ifeq2da.1 | . . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐴 = 𝐵) | |
| 6 | 5 | ifeq2d 4545 | . 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) | 
| 7 | 4, 6 | pm2.61dan 812 | 1 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 = wceq 1539 ifcif 4524 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-rab 3436 df-v 3481 df-un 3955 df-if 4525 | 
| This theorem is referenced by: ifeq12da 4558 dfac12lem1 10185 ttukeylem3 10552 xmulcom 13309 xmulneg1 13312 subgmulg 19159 1marepvmarrepid 22582 pcopt2 25057 limcdif 25912 limcmpt 25919 limcres 25922 limccnp 25927 radcnv0 26460 leibpi 26986 efrlim 27013 efrlimOLD 27014 dchrvmasumiflem2 27547 padicabvf 27676 padicabvcxp 27677 itg2addnclem 37679 fourierdlem73 46199 fourierdlem76 46202 fourierdlem89 46215 fourierdlem91 46217 | 
| Copyright terms: Public domain | W3C validator |