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

Theorem ifeq2d 4096
Description: Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.)
Hypothesis
Ref Expression
ifeq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
ifeq2d (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))

Proof of Theorem ifeq2d
StepHypRef Expression
1 ifeq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 ifeq2 4082 . 2 (𝐴 = 𝐵 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
31, 2syl 17 1 (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  ifcif 4077
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-v 3197  df-un 3572  df-if 4078
This theorem is referenced by:  ifeq12d  4097  ifbieq2d  4102  ifeq2da  4108  ifcomnan  4128  rdgeq1  7492  cantnflem1d  8570  cantnflem1  8571  rexmul  12086  1arithlem4  15611  ramcl  15714  mplcoe1  19446  mplcoe5  19449  subrgascl  19479  scmatscm  20300  marrepfval  20347  ma1repveval  20358  mulmarep1el  20359  mdetralt2  20396  mdetunilem8  20406  maduval  20425  maducoeval2  20427  madurid  20431  minmar1val0  20434  monmatcollpw  20565  pmatcollpwscmatlem1  20575  monmat2matmon  20610  itg2monolem1  23498  iblmulc2  23578  itgmulc2lem1  23579  bddmulibl  23586  dvtaylp  24105  dchrinvcl  24959  rpvmasum2  25182  padicfval  25286  plymulx  30599  itg2addnclem  33432  itg2addnclem3  33434  itg2addnc  33435  itgmulc2nclem1  33447  hdmap1fval  36905  itgioocnicc  39956  etransclem14  40228  etransclem17  40231  etransclem21  40235  etransclem25  40239  etransclem28  40242  etransclem31  40245  hsphoif  40553  hoidmvval  40554  hsphoival  40556  hoidmvlelem5  40576  hoidmvle  40577  ovnhoi  40580  hspmbllem2  40604
  Copyright terms: Public domain W3C validator