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

Theorem ifeq2da 4089
 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 4064 . . . 4 (𝜓 → if(𝜓, 𝐶, 𝐴) = 𝐶)
2 iftrue 4064 . . . 4 (𝜓 → if(𝜓, 𝐶, 𝐵) = 𝐶)
31, 2eqtr4d 2658 . . 3 (𝜓 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
43adantl 482 . 2 ((𝜑𝜓) → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
5 ifeq2da.1 . . 3 ((𝜑 ∧ ¬ 𝜓) → 𝐴 = 𝐵)
65ifeq2d 4077 . 2 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
74, 6pm2.61dan 831 1 (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 384   = wceq 1480  ifcif 4058 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2916  df-v 3188  df-un 3560  df-if 4059 This theorem is referenced by:  ifeq12da  4090  dfac12lem1  8909  ttukeylem3  9277  xmulcom  12039  xmulneg1  12042  subgmulg  17529  1marepvmarrepid  20300  copco  22726  pcopt2  22731  limcdif  23546  limcmpt  23553  limcres  23556  limccnp  23561  radcnv0  24074  leibpi  24569  efrlim  24596  dchrvmasumiflem2  25091  rpvmasum2  25101  padicabvf  25220  padicabvcxp  25221  itg2addnclem  33093  fourierdlem73  39703  fourierdlem76  39706  fourierdlem89  39719  fourierdlem91  39721
 Copyright terms: Public domain W3C validator