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

Theorem ifeq1d 4095
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 4081 . 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  ifbieq1d  4100  ifeq1da  4107  rabsnif  4249  fsuppmptif  8290  cantnflem1  8571  sumeq2w  14403  cbvsum  14406  isumless  14558  prodss  14658  subgmulg  17589  evlslem2  19493  dmatcrng  20289  scmatscmiddistr  20295  scmatcrng  20308  marrepfval  20347  mdetr0  20392  mdetunilem8  20406  madufval  20424  madugsum  20430  minmar1fval  20433  decpmatid  20556  monmatcollpw  20565  pmatcollpwscmatlem1  20575  cnmpt2pc  22708  pcoval2  22797  pcopt  22803  itgz  23528  iblss2  23553  itgss  23559  itgcn  23590  plyeq0lem  23947  dgrcolem2  24011  plydivlem4  24032  leibpi  24650  chtublem  24917  sumdchr  24978  bposlem6  24995  lgsval  25007  dchrvmasumiflem2  25172  padicabvcxp  25302  dfrdg3  31676  matunitlindflem1  33376  ftc1anclem2  33457  ftc1anclem5  33460  ftc1anclem7  33462  hoidifhspval  40585  hoimbl  40608
  Copyright terms: Public domain W3C validator