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

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

Proof of Theorem ifeq2da
StepHypRef Expression
1 iftrue 4530 . . . 4 (𝜓 → if(𝜓, 𝐶, 𝐴) = 𝐶)
2 iftrue 4530 . . . 4 (𝜓 → if(𝜓, 𝐶, 𝐵) = 𝐶)
31, 2eqtr4d 2779 . . 3 (𝜓 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
43adantl 481 . 2 ((𝜑𝜓) → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
5 ifeq2da.1 . . 3 ((𝜑 ∧ ¬ 𝜓) → 𝐴 = 𝐵)
65ifeq2d 4545 . 2 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
74, 6pm2.61dan 812 1 (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395   = wceq 1539  ifcif 4524
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-un 3955  df-if 4525
This theorem is referenced by:  ifeq12da  4558  dfac12lem1  10185  ttukeylem3  10552  xmulcom  13309  xmulneg1  13312  subgmulg  19159  1marepvmarrepid  22582  pcopt2  25057  limcdif  25912  limcmpt  25919  limcres  25922  limccnp  25927  radcnv0  26460  leibpi  26986  efrlim  27013  efrlimOLD  27014  dchrvmasumiflem2  27547  padicabvf  27676  padicabvcxp  27677  itg2addnclem  37679  fourierdlem73  46199  fourierdlem76  46202  fourierdlem89  46215  fourierdlem91  46217
  Copyright terms: Public domain W3C validator