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

Theorem ifeq1d 3579
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 3569 . 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 1623   ifcif 3565
This theorem is referenced by:  ifeq12d  3581  ifeq1da  3590  cantnflem1d  7390  cantnflem1  7391  isumless  12304  subgmulg  14635  gsumzsplit  15206  evlslem2  16249  cnmpt2pc  18426  pcoval2  18514  pcopt  18520  itgz  19135  iblss2  19160  itgss  19166  itgcn  19197  plyeq0lem  19592  dgrcolem2  19655  plydivlem4  19676  leibpi  20238  chtublem  20450  sumdchr  20511  bposlem6  20528  lgsval  20539  dchrvmasumiflem2  20651  padicabvcxp  20781  dfrdg3  24153  linevala2  26078  sgplpte21  26132  sgplpte22  26138  isray2  26153  isray  26154
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-un 3157  df-if 3566
  Copyright terms: Public domain W3C validator