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

Theorem ifeq2da 4273
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 4248 . . . 4 (𝜓 → if(𝜓, 𝐶, 𝐴) = 𝐶)
2 iftrue 4248 . . . 4 (𝜓 → if(𝜓, 𝐶, 𝐵) = 𝐶)
31, 2eqtr4d 2801 . . 3 (𝜓 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
43adantl 473 . 2 ((𝜑𝜓) → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
5 ifeq2da.1 . . 3 ((𝜑 ∧ ¬ 𝜓) → 𝐴 = 𝐵)
65ifeq2d 4261 . 2 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
74, 6pm2.61dan 847 1 (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384   = wceq 1652  ifcif 4242
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-rab 3063  df-v 3351  df-un 3736  df-if 4243
This theorem is referenced by:  ifeq12da  4274  dfac12lem1  9217  ttukeylem3  9585  xmulcom  12297  xmulneg1  12300  subgmulg  17873  1marepvmarrepid  20657  copco  23095  pcopt2  23100  limcdif  23930  limcmpt  23937  limcres  23940  limccnp  23945  radcnv0  24460  leibpi  24959  efrlim  24986  dchrvmasumiflem2  25481  rpvmasum2  25491  padicabvf  25610  padicabvcxp  25611  itg2addnclem  33816  fourierdlem73  40965  fourierdlem76  40968  fourierdlem89  40981  fourierdlem91  40983
  Copyright terms: Public domain W3C validator