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

Theorem ifeq1d 3520
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 3510 . 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 set class
Syntax hints:    -> wi 6    = wceq 1619   ifcif 3506
This theorem is referenced by:  ifeq12d  3522  ifeq1da  3531  cantnflem1d  7323  cantnflem1  7324  isumless  12231  subgmulg  14562  gsumzsplit  15133  evlslem2  16176  cnmpt2pc  18353  pcoval2  18441  pcopt  18447  itgz  19062  iblss2  19087  itgss  19093  itgcn  19124  plyeq0lem  19519  dgrcolem2  19582  plydivlem4  19603  leibpi  20165  chtublem  20377  sumdchr  20438  bposlem6  20455  lgsval  20466  dchrvmasumiflem2  20578  padicabvcxp  20708  dfrdg3  23487  linevala2  25410  sgplpte21  25464  sgplpte22  25470  isray2  25485  isray  25486
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-rab 2523  df-v 2742  df-un 3099  df-if 3507
  Copyright terms: Public domain W3C validator