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

Theorem ifeq2da 4067
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 4042 . . . 4 (𝜓 → if(𝜓, 𝐶, 𝐴) = 𝐶)
2 iftrue 4042 . . . 4 (𝜓 → if(𝜓, 𝐶, 𝐵) = 𝐶)
31, 2eqtr4d 2647 . . 3 (𝜓 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
43adantl 481 . 2 ((𝜑𝜓) → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
5 ifeq2da.1 . . 3 ((𝜑 ∧ ¬ 𝜓) → 𝐴 = 𝐵)
65ifeq2d 4055 . 2 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
74, 6pm2.61dan 828 1 (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383   = wceq 1475  ifcif 4036
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-un 3545  df-if 4037
This theorem is referenced by:  ifeq12da  4068  dfac12lem1  8848  ttukeylem3  9216  xmulcom  11968  xmulneg1  11971  subgmulg  17431  1marepvmarrepid  20200  copco  22626  pcopt2  22631  limcdif  23446  limcmpt  23453  limcres  23456  limccnp  23461  radcnv0  23974  leibpi  24469  efrlim  24496  dchrvmasumiflem2  24991  rpvmasum2  25001  padicabvf  25120  padicabvcxp  25121  itg2addnclem  32631  fourierdlem73  39072  fourierdlem76  39075  fourierdlem89  39088  fourierdlem91  39090
  Copyright terms: Public domain W3C validator