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

Theorem ifeqda 4261
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 4232 . . . 4 (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
21adantl 467 . . 3 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3 ifeqda.1 . . 3 ((𝜑𝜓) → 𝐴 = 𝐶)
42, 3eqtrd 2805 . 2 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
5 iffalse 4235 . . . 4 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
65adantl 467 . . 3 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7 ifeqda.2 . . 3 ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶)
86, 7eqtrd 2805 . 2 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
94, 8pm2.61dan 814 1 (𝜑 → if(𝜓, 𝐴, 𝐵) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382   = wceq 1631  ifcif 4226
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-if 4227
This theorem is referenced by:  somincom  5670  cantnfp1  8746  ccatsymb  13564  swrdccat3blem  13704  repswccat  13741  ccatco  13790  bitsinvp1  15379  xrsdsreval  20006  fvmptnn04if  20874  chfacfscmulgsum  20885  chfacfpmmulgsum  20889  oprpiece1res2  22971  phtpycc  23010  atantayl2  24886  ifeq3da  29703  fprodex01  29911  psgnfzto1stlem  30190  fzto1st1  30192  mdetlap1  30232  madjusmdetlem1  30233  madjusmdetlem2  30234  ccatmulgnn0dir  30959  plymulx  30965  itgexpif  31024  repr0  31029  elmrsubrn  31755  matunitlindflem1  33738  fourierdlem101  40938  hoidmv1lelem2  41323  linc0scn0  42737  m1modmmod  42841  digexp  42926
  Copyright terms: Public domain W3C validator