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

Theorem ifeq1da 4557
Description: Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.)
Hypothesis
Ref Expression
ifeq1da.1 ((𝜑𝜓) → 𝐴 = 𝐵)
Assertion
Ref Expression
ifeq1da (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))

Proof of Theorem ifeq1da
StepHypRef Expression
1 ifeq1da.1 . . 3 ((𝜑𝜓) → 𝐴 = 𝐵)
21ifeq1d 4545 . 2 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3 iffalse 4534 . . . 4 𝜓 → if(𝜓, 𝐴, 𝐶) = 𝐶)
4 iffalse 4534 . . . 4 𝜓 → if(𝜓, 𝐵, 𝐶) = 𝐶)
53, 4eqtr4d 2780 . . 3 𝜓 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
65adantl 481 . 2 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
72, 6pm2.61dan 813 1 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395   = wceq 1540  ifcif 4525
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-un 3956  df-if 4526
This theorem is referenced by:  ifeq12da  4559  cantnflem1d  9728  cantnflem1  9729  dfac12lem1  10184  xrmaxeq  13221  xrmineq  13222  rexmul  13313  max0add  15349  sumeq2ii  15729  fsumser  15766  ramcl  17067  dmdprdsplitlem  20057  coe1pwmul  22282  scmatscmiddistr  22514  mulmarep1gsum1  22579  maducoeval2  22646  madugsum  22649  madurid  22650  ptcld  23621  ibllem  25799  itgvallem3  25821  iblposlem  25827  iblss2  25841  iblmulc2  25866  cnplimc  25922  limcco  25928  dvexp3  26016  dchrinvcl  27297  lgsval2lem  27351  lgsval4lem  27352  lgsneg  27365  lgsmod  27367  lgsdilem2  27377  rpvmasum2  27556  mrsubrn  35518  ftc1anclem6  37705  ftc1anclem8  37707  fsuppind  42600
  Copyright terms: Public domain W3C validator