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 4469 | . . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴) | |
2 | 1 | adantl 482 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴) |
3 | ifeqda.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶) | |
4 | 2, 3 | eqtrd 2853 | . 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶) |
5 | iffalse 4472 | . . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵) | |
6 | 5 | adantl 482 | . . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵) |
7 | ifeqda.2 | . . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶) | |
8 | 6, 7 | eqtrd 2853 | . 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶) |
9 | 4, 8 | pm2.61dan 809 | 1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 = wceq 1528 ifcif 4463 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-ex 1772 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-if 4464 |
This theorem is referenced by: somincom 5987 cantnfp1 9132 ccatsymb 13924 swrdccat3blem 14089 repswccat 14136 ccatco 14185 bitsinvp1 15786 xrsdsreval 20518 fvmptnn04if 21385 chfacfscmulgsum 21396 chfacfpmmulgsum 21400 oprpiece1res2 23483 phtpycc 23522 atantayl2 25443 ifeq3da 30228 fprodex01 30468 psgnfzto1stlem 30669 fzto1st1 30671 cycpm2tr 30688 mdetlap1 30990 madjusmdetlem1 30991 madjusmdetlem2 30992 ccatmulgnn0dir 31711 plymulx 31717 itgexpif 31776 repr0 31781 elmrsubrn 32664 matunitlindflem1 34769 frlmvscadiccat 39023 fourierdlem101 42369 hoidmv1lelem2 42751 dfafv2 43208 linc0scn0 44406 m1modmmod 44509 digexp 44595 |
Copyright terms: Public domain | W3C validator |