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

Theorem ifeq2da 4561
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 4535 . . . 4 (𝜓 → if(𝜓, 𝐶, 𝐴) = 𝐶)
2 iftrue 4535 . . . 4 (𝜓 → if(𝜓, 𝐶, 𝐵) = 𝐶)
31, 2eqtr4d 2776 . . 3 (𝜓 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
43adantl 483 . 2 ((𝜑𝜓) → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
5 ifeq2da.1 . . 3 ((𝜑 ∧ ¬ 𝜓) → 𝐴 = 𝐵)
65ifeq2d 4549 . 2 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
74, 6pm2.61dan 812 1 (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397   = wceq 1542  ifcif 4529
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-un 3954  df-if 4530
This theorem is referenced by:  ifeq12da  4562  dfac12lem1  10138  ttukeylem3  10506  xmulcom  13245  xmulneg1  13248  subgmulg  19020  1marepvmarrepid  22077  pcopt2  24539  limcdif  25393  limcmpt  25400  limcres  25403  limccnp  25408  radcnv0  25928  leibpi  26447  efrlim  26474  dchrvmasumiflem2  27005  padicabvf  27134  padicabvcxp  27135  itg2addnclem  36539  fourierdlem73  44895  fourierdlem76  44898  fourierdlem89  44911  fourierdlem91  44913
  Copyright terms: Public domain W3C validator