![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ifeqda | Structured version Visualization version GIF version |
Description: Separation of the values of the conditional operator. (Contributed by Alexander van der Vekens, 13-Apr-2018.) |
Ref | Expression |
---|---|
ifeqda.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶) |
ifeqda.2 | ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
ifeqda | ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iftrue 4536 | . . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴) | |
2 | 1 | adantl 480 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴) |
3 | ifeqda.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶) | |
4 | 2, 3 | eqtrd 2765 | . 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶) |
5 | iffalse 4539 | . . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵) | |
6 | 5 | adantl 480 | . . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵) |
7 | ifeqda.2 | . . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶) | |
8 | 6, 7 | eqtrd 2765 | . 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶) |
9 | 4, 8 | pm2.61dan 811 | 1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 394 = wceq 1533 ifcif 4530 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-if 4531 |
This theorem is referenced by: somincom 6141 cantnfp1 9706 ccatsymb 14568 swrdccat3blem 14725 repswccat 14772 ccatco 14822 bitsinvp1 16427 xrsdsreval 21361 fvmptnn04if 22795 chfacfscmulgsum 22806 chfacfpmmulgsum 22810 oprpiece1res2 24921 phtpycc 24961 atantayl2 26915 ifeq3da 32416 fprodex01 32673 psgnfzto1stlem 32913 fzto1st1 32915 cycpm2tr 32932 elrspunsn 33241 mdetlap1 33555 madjusmdetlem1 33556 madjusmdetlem2 33557 ccatmulgnn0dir 34302 plymulx 34308 itgexpif 34366 repr0 34371 elmrsubrn 35258 matunitlindflem1 37217 sticksstones12 41758 frlmvscadiccat 41881 fsuppind 41955 fsuppssindlem1 41956 reabsifneg 43201 reabsifnpos 43202 reabsifpos 43203 reabsifnneg 43204 reabssgn 43205 sqrtcval 43210 mnringmulrcld 43804 fourierdlem101 45730 hoidmv1lelem2 46115 dfafv2 46647 linc0scn0 47674 m1modmmod 47777 digexp 47863 |
Copyright terms: Public domain | W3C validator |