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

Theorem ifeq1d 3898
Description: Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.)
Hypothesis
Ref Expression
ifeq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
ifeq1d  |-  ( ph  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)

Proof of Theorem ifeq1d
StepHypRef Expression
1 ifeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 ifeq1 3884 . 2  |-  ( A  =  B  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C ) )
31, 2syl 17 1  |-  ( ph  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1443   ifcif 3880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-rab 2745  df-v 3046  df-un 3408  df-if 3881
This theorem is referenced by:  ifeq12d  3900  ifbieq1d  3903  ifeq1da  3910  rabsnif  4040  fsuppmptif  7910  cantnflem1  8191  sumeq2w  13751  cbvsum  13754  isumless  13896  prodss  13994  subgmulg  16824  evlslem2  18728  dmatcrng  19520  scmatscmiddistr  19526  scmatcrng  19539  marrepfval  19578  mdetr0  19623  mdetunilem8  19637  madufval  19655  madugsum  19661  minmar1fval  19664  decpmatid  19787  monmatcollpw  19796  pmatcollpwscmatlem1  19806  cnmpt2pc  21949  pcoval2  22040  pcopt  22046  itgz  22731  iblss2  22756  itgss  22762  itgcn  22793  plyeq0lem  23157  dgrcolem2  23221  plydivlem4  23242  leibpi  23861  chtublem  24132  sumdchr  24193  bposlem6  24210  lgsval  24221  dchrvmasumiflem2  24333  padicabvcxp  24463  dfrdg3  30436  ftc1anclem2  32011  ftc1anclem5  32014  ftc1anclem7  32016  hoidifhspval  38424  hoimbl  38447
  Copyright terms: Public domain W3C validator