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

Theorem ifeq1d 3903
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 3889 . 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 setvar class
Syntax hints:    -> wi 4    = wceq 1405   ifcif 3885
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rab 2763  df-v 3061  df-un 3419  df-if 3886
This theorem is referenced by:  ifeq12d  3905  ifbieq1d  3908  ifeq1da  3915  rabsnif  4041  fsuppmptif  7893  cantnflem1  8140  cantnflem1dOLD  8162  cantnflem1OLD  8163  sumeq2w  13663  cbvsum  13666  isumless  13808  prodss  13906  subgmulg  16539  gsumzsplitOLD  17269  evlslem2  18500  dmatcrng  19296  scmatscmiddistr  19302  scmatcrng  19315  marrepfval  19354  mdetr0  19399  mdetunilem8  19413  madufval  19431  madugsum  19437  minmar1fval  19440  decpmatid  19563  monmatcollpw  19572  pmatcollpwscmatlem1  19582  cnmpt2pc  21720  pcoval2  21808  pcopt  21814  itgz  22479  iblss2  22504  itgss  22510  itgcn  22541  plyeq0lem  22899  dgrcolem2  22963  plydivlem4  22984  leibpi  23598  chtublem  23867  sumdchr  23928  bposlem6  23945  lgsval  23956  dchrvmasumiflem2  24068  padicabvcxp  24198  dfrdg3  30016  ftc1anclem2  31464  ftc1anclem5  31467  ftc1anclem7  31469
  Copyright terms: Public domain W3C validator