| 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 4531 | . . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴) | |
| 2 | 1 | adantl 481 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴) |
| 3 | ifeqda.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶) | |
| 4 | 2, 3 | eqtrd 2777 | . 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶) |
| 5 | iffalse 4534 | . . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵) | |
| 6 | 5 | adantl 481 | . . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵) |
| 7 | ifeqda.2 | . . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶) | |
| 8 | 6, 7 | eqtrd 2777 | . 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶) |
| 9 | 4, 8 | pm2.61dan 813 | 1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = 𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 = wceq 1540 ifcif 4525 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-if 4526 |
| This theorem is referenced by: somincom 6154 cantnfp1 9721 ccatsymb 14620 swrdccat3blem 14777 repswccat 14824 ccatco 14874 bitsinvp1 16486 xrsdsreval 21429 fvmptnn04if 22855 chfacfscmulgsum 22866 chfacfpmmulgsum 22870 oprpiece1res2 24983 phtpycc 25023 atantayl2 26981 ifeq3da 32559 fprodex01 32827 psgnfzto1stlem 33120 fzto1st1 33122 cycpm2tr 33139 elrgspnlem4 33249 elrspunsn 33457 fldextrspunlsp 33724 mdetlap1 33825 madjusmdetlem1 33826 madjusmdetlem2 33827 ccatmulgnn0dir 34557 plymulx 34563 itgexpif 34621 repr0 34626 elmrsubrn 35525 matunitlindflem1 37623 sticksstones12 42159 redvmptabs 42390 readvrec 42392 frlmvscadiccat 42516 fsuppind 42600 fsuppssindlem1 42601 reabsifneg 43645 reabsifnpos 43646 reabsifpos 43647 reabsifnneg 43648 reabssgn 43649 sqrtcval 43654 mnringmulrcld 44247 fourierdlem101 46222 hoidmv1lelem2 46607 dfafv2 47144 linc0scn0 48340 m1modmmod 48442 digexp 48528 |
| Copyright terms: Public domain | W3C validator |