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

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

Proof of Theorem ifeq1d
StepHypRef Expression
1 ifeq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 ifeq1 4226 . 2 (𝐴 = 𝐵 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
31, 2syl 17 1 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1624  ifcif 4222
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-rab 3051  df-v 3334  df-un 3712  df-if 4223
This theorem is referenced by:  ifeq12d  4242  ifbieq1d  4245  ifeq1da  4252  rabsnif  4394  fsuppmptif  8462  cantnflem1  8751  sumeq2w  14613  cbvsum  14616  isumless  14768  prodss  14868  subgmulg  17801  evlslem2  19706  dmatcrng  20502  scmatscmiddistr  20508  scmatcrng  20521  marrepfval  20560  mdetr0  20605  mdetunilem8  20619  madufval  20637  madugsum  20643  minmar1fval  20646  decpmatid  20769  monmatcollpw  20778  pmatcollpwscmatlem1  20788  cnmpt2pc  22920  pcoval2  23008  pcopt  23014  itgz  23738  iblss2  23763  itgss  23769  itgcn  23800  plyeq0lem  24157  dgrcolem2  24221  plydivlem4  24242  leibpi  24860  chtublem  25127  sumdchr  25188  bposlem6  25205  lgsval  25217  dchrvmasumiflem2  25382  padicabvcxp  25512  dfrdg3  31999  matunitlindflem1  33710  ftc1anclem2  33791  ftc1anclem5  33794  ftc1anclem7  33796  hoidifhspval  41320  hoimbl  41343
  Copyright terms: Public domain W3C validator