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

Theorem ifeq2d 4326
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 4312 . 2 (𝐴 = 𝐵 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
31, 2syl 17 1 (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1601  ifcif 4307
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-v 3400  df-un 3797  df-if 4308
This theorem is referenced by:  ifeq12d  4327  ifbieq2d  4332  ifeq2da  4338  ifcomnan  4361  rdgeq1  7792  cantnflem1d  8884  cantnflem1  8885  rexmul  12417  1arithlem4  16038  ramcl  16141  mplcoe1  19866  mplcoe5  19869  subrgascl  19898  scmatscm  20728  marrepfval  20775  ma1repveval  20786  mulmarep1el  20787  mdetralt2  20824  mdetunilem8  20834  maduval  20853  maducoeval2  20855  madurid  20859  minmar1val0  20862  monmatcollpw  20995  pmatcollpwscmatlem1  21005  monmat2matmon  21040  itg2monolem1  23958  iblmulc2  24038  itgmulc2lem1  24039  bddmulibl  24046  dvtaylp  24565  dchrinvcl  25434  rpvmasum2  25657  padicfval  25761  plymulx  31229  itg2addnclem  34091  itg2addnclem3  34093  itg2addnc  34094  itgmulc2nclem1  34106  hdmap1fval  37955  itgioocnicc  41130  etransclem14  41402  etransclem17  41405  etransclem21  41409  etransclem25  41413  etransclem28  41416  etransclem31  41419  hsphoif  41727  hoidmvval  41728  hsphoival  41730  hoidmvlelem5  41750  hoidmvle  41751  ovnhoi  41754  hspmbllem2  41778
  Copyright terms: Public domain W3C validator