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 4042 | . . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴) | |
2 | 1 | adantl 481 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴) |
3 | ifeqda.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶) | |
4 | 2, 3 | eqtrd 2644 | . 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶) |
5 | iffalse 4045 | . . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵) | |
6 | 5 | adantl 481 | . . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵) |
7 | ifeqda.2 | . . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶) | |
8 | 6, 7 | eqtrd 2644 | . 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶) |
9 | 4, 8 | pm2.61dan 828 | 1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 383 = wceq 1475 ifcif 4036 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-if 4037 |
This theorem is referenced by: somincom 5449 cantnfp1 8461 ccatsymb 13219 swrdccat3blem 13346 repswccat 13383 ccatco 13432 bitsinvp1 15009 xrsdsreval 19610 fvmptnn04if 20473 chfacfscmulgsum 20484 chfacfpmmulgsum 20488 oprpiece1res2 22559 phtpycc 22598 atantayl2 24465 psgnfzto1stlem 29181 fzto1st1 29183 mdetlap1 29220 madjusmdetlem1 29221 madjusmdetlem2 29222 ccatmulgnn0dir 29945 plymulx 29951 elmrsubrn 30671 matunitlindflem1 32575 fourierdlem101 39100 hoidmv1lelem2 39482 linc0scn0 42006 m1modmmod 42110 digexp 42199 |
Copyright terms: Public domain | W3C validator |