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

Theorem ifeq1d 3581
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 3571 . 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 1624   ifcif 3567
This theorem is referenced by:  ifeq12d  3583  ifeq1da  3592  cantnflem1d  7386  cantnflem1  7387  isumless  12299  subgmulg  14630  gsumzsplit  15201  evlslem2  16244  cnmpt2pc  18421  pcoval2  18509  pcopt  18515  itgz  19130  iblss2  19155  itgss  19161  itgcn  19192  plyeq0lem  19587  dgrcolem2  19650  plydivlem4  19671  leibpi  20233  chtublem  20445  sumdchr  20506  bposlem6  20523  lgsval  20534  dchrvmasumiflem2  20646  padicabvcxp  20776  dfrdg3  23555  linevala2  25478  sgplpte21  25532  sgplpte22  25538  isray2  25553  isray  25554
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rab 2554  df-v 2792  df-un 3159  df-if 3568
  Copyright terms: Public domain W3C validator