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

Theorem ifeq1d 3592
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 3582 . 2  |-  ( A  =  B  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C ) )
31, 2syl 15 1  |-  ( ph  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   ifcif 3578
This theorem is referenced by:  ifeq12d  3594  ifeq1da  3603  cantnflem1d  7406  cantnflem1  7407  isumless  12320  subgmulg  14651  gsumzsplit  15222  evlslem2  16265  cnmpt2pc  18442  pcoval2  18530  pcopt  18536  itgz  19151  iblss2  19176  itgss  19182  itgcn  19213  plyeq0lem  19608  dgrcolem2  19671  plydivlem4  19692  leibpi  20254  chtublem  20466  sumdchr  20527  bposlem6  20544  lgsval  20555  dchrvmasumiflem2  20667  padicabvcxp  20797  dfrdg3  24224  linevala2  26181  sgplpte21  26235  sgplpte22  26241  isray2  26256  isray  26257
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-un 3170  df-if 3579
  Copyright terms: Public domain W3C validator