MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ifeqda Structured version   Visualization version   GIF version

Theorem ifeqda 4498
Description: Separation of the values of the conditional operator. (Contributed by Alexander van der Vekens, 13-Apr-2018.)
Hypotheses
Ref Expression
ifeqda.1 ((𝜑𝜓) → 𝐴 = 𝐶)
ifeqda.2 ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶)
Assertion
Ref Expression
ifeqda (𝜑 → if(𝜓, 𝐴, 𝐵) = 𝐶)

Proof of Theorem ifeqda
StepHypRef Expression
1 iftrue 4469 . . . 4 (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
21adantl 482 . . 3 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3 ifeqda.1 . . 3 ((𝜑𝜓) → 𝐴 = 𝐶)
42, 3eqtrd 2853 . 2 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
5 iffalse 4472 . . . 4 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
65adantl 482 . . 3 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7 ifeqda.2 . . 3 ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶)
86, 7eqtrd 2853 . 2 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
94, 8pm2.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