![]() |
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 4431 | . . . 4 ⊢ (𝜓 → if(𝜓, 𝐶, 𝐴) = 𝐶) | |
2 | iftrue 4431 | . . . 4 ⊢ (𝜓 → if(𝜓, 𝐶, 𝐵) = 𝐶) | |
3 | 1, 2 | eqtr4d 2836 | . . 3 ⊢ (𝜓 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) |
4 | 3 | adantl 485 | . 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) |
5 | ifeq2da.1 | . . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐴 = 𝐵) | |
6 | 5 | ifeq2d 4444 | . 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 399 = wceq 1538 ifcif 4425 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-12 2175 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-rab 3115 df-v 3443 df-un 3886 df-if 4426 |
This theorem is referenced by: ifeq12da 4457 dfac12lem1 9554 ttukeylem3 9922 xmulcom 12647 xmulneg1 12650 subgmulg 18285 1marepvmarrepid 21180 pcopt2 23628 limcdif 24479 limcmpt 24486 limcres 24489 limccnp 24494 radcnv0 25011 leibpi 25528 efrlim 25555 dchrvmasumiflem2 26086 padicabvf 26215 padicabvcxp 26216 itg2addnclem 35108 fourierdlem73 42821 fourierdlem76 42824 fourierdlem89 42837 fourierdlem91 42839 |
Copyright terms: Public domain | W3C validator |