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

Theorem ifeq1d 3907
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 3895 . 2  |-  ( A  =  B  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C ) )
31, 2syl 16 1  |-  ( ph  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370   ifcif 3891
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rab 2804  df-v 3072  df-un 3433  df-if 3892
This theorem is referenced by:  ifeq12d  3909  ifbieq1d  3912  ifeq1da  3919  rabsnif  4044  fsuppmptif  7752  cantnflem1d  7999  cantnflem1  8000  cantnflem1dOLD  8022  cantnflem1OLD  8023  cbvsum  13276  isumless  13412  subgmulg  15799  gsumzsplitOLD  16525  evlslem2  17706  marrepfval  18484  mdetr0  18529  mdetunilem8  18543  madufval  18561  madugsum  18567  minmar1fval  18570  cnmpt2pc  20618  pcoval2  20706  pcopt  20712  itgz  21376  iblss2  21401  itgss  21407  itgcn  21438  plyeq0lem  21796  dgrcolem2  21859  plydivlem4  21880  leibpi  22455  chtublem  22668  sumdchr  22729  bposlem6  22746  lgsval  22757  dchrvmasumiflem2  22869  padicabvcxp  22999  prodss  27596  dfrdg3  27746  ftc1anclem2  28608  ftc1anclem5  28611  ftc1anclem7  28613  dmatcrng  31037  scmatmulcl  31042  scmatcrng  31044  pmatcollpw1id  31228  monmatcollpw  31238  pmatcollpwscmatlem1  31247
  Copyright terms: Public domain W3C validator