![]() |
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 4534 | . . . 4 ⊢ (𝜓 → if(𝜓, 𝐶, 𝐴) = 𝐶) | |
2 | iftrue 4534 | . . . 4 ⊢ (𝜓 → if(𝜓, 𝐶, 𝐵) = 𝐶) | |
3 | 1, 2 | eqtr4d 2774 | . . 3 ⊢ (𝜓 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) |
4 | 3 | adantl 481 | . 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) |
5 | ifeq2da.1 | . . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐴 = 𝐵) | |
6 | 5 | ifeq2d 4548 | . 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) |
7 | 4, 6 | pm2.61dan 810 | 1 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 = wceq 1540 ifcif 4528 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-tru 1543 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-rab 3432 df-v 3475 df-un 3953 df-if 4529 |
This theorem is referenced by: ifeq12da 4561 dfac12lem1 10144 ttukeylem3 10512 xmulcom 13252 xmulneg1 13255 subgmulg 19063 1marepvmarrepid 22397 pcopt2 24870 limcdif 25725 limcmpt 25732 limcres 25735 limccnp 25740 radcnv0 26267 leibpi 26788 efrlim 26815 dchrvmasumiflem2 27348 padicabvf 27477 padicabvcxp 27478 itg2addnclem 37003 fourierdlem73 45354 fourierdlem76 45357 fourierdlem89 45370 fourierdlem91 45372 |
Copyright terms: Public domain | W3C validator |