![]() |
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 4312 | . . . 4 ⊢ (𝜓 → if(𝜓, 𝐶, 𝐴) = 𝐶) | |
2 | iftrue 4312 | . . . 4 ⊢ (𝜓 → if(𝜓, 𝐶, 𝐵) = 𝐶) | |
3 | 1, 2 | eqtr4d 2864 | . . 3 ⊢ (𝜓 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) |
4 | 3 | adantl 475 | . 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) |
5 | ifeq2da.1 | . . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐴 = 𝐵) | |
6 | 5 | ifeq2d 4325 | . 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) |
7 | 4, 6 | pm2.61dan 847 | 1 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 386 = wceq 1656 ifcif 4306 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-13 2389 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-rab 3126 df-v 3416 df-un 3803 df-if 4307 |
This theorem is referenced by: ifeq12da 4338 dfac12lem1 9280 ttukeylem3 9648 xmulcom 12384 xmulneg1 12387 subgmulg 17959 1marepvmarrepid 20749 copco 23187 pcopt2 23192 limcdif 24039 limcmpt 24046 limcres 24049 limccnp 24054 radcnv0 24569 leibpi 25082 efrlim 25109 dchrvmasumiflem2 25604 rpvmasum2 25614 padicabvf 25733 padicabvcxp 25734 itg2addnclem 33997 fourierdlem73 41183 fourierdlem76 41186 fourierdlem89 41199 fourierdlem91 41201 |
Copyright terms: Public domain | W3C validator |