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

Theorem ifeqda 4066
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 4037 . . . 4 (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
21adantl 480 . . 3 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3 ifeqda.1 . . 3 ((𝜑𝜓) → 𝐴 = 𝐶)
42, 3eqtrd 2639 . 2 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
5 iffalse 4040 . . . 4 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
65adantl 480 . . 3 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7 ifeqda.2 . . 3 ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶)
86, 7eqtrd 2639 . 2 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
94, 8pm2.61dan 827 1 (𝜑 → if(𝜓, 𝐴, 𝐵) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382   = wceq 1474  ifcif 4031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-if 4032
This theorem is referenced by:  somincom  5432  cantnfp1  8434  ccatsymb  13161  swrdccat3blem  13288  repswccat  13325  ccatco  13374  bitsinvp1  14951  xrsdsreval  19552  fvmptnn04if  20411  chfacfscmulgsum  20422  chfacfpmmulgsum  20426  oprpiece1res2  22486  phtpycc  22525  atantayl2  24378  psgnfzto1stlem  28983  fzto1st1  28985  mdetlap1  29022  madjusmdetlem1  29023  madjusmdetlem2  29024  ccatmulgnn0dir  29747  plymulx  29753  elmrsubrn  30473  matunitlindflem1  32374  fourierdlem101  38900  hoidmv1lelem2  39282  linc0scn0  42004  m1modmmod  42108  digexp  42197
  Copyright terms: Public domain W3C validator