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

Theorem ifeq1d 3950
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 3936 . 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 1374   ifcif 3932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-rab 2816  df-v 3108  df-un 3474  df-if 3933
This theorem is referenced by:  ifeq12d  3952  ifbieq1d  3955  ifeq1da  3962  rabsnif  4089  fsuppmptif  7848  cantnflem1d  8096  cantnflem1  8097  cantnflem1dOLD  8119  cantnflem1OLD  8120  cbvsum  13466  isumless  13609  subgmulg  16003  gsumzsplitOLD  16729  evlslem2  17944  dmatcrng  18764  scmatscmiddistr  18770  scmatcrng  18783  marrepfval  18822  mdetr0  18867  mdetunilem8  18881  madufval  18899  madugsum  18905  minmar1fval  18908  decpmatid  19031  monmatcollpw  19040  pmatcollpwscmatlem1  19050  cnmpt2pc  21156  pcoval2  21244  pcopt  21250  itgz  21915  iblss2  21940  itgss  21946  itgcn  21977  plyeq0lem  22335  dgrcolem2  22398  plydivlem4  22419  leibpi  22994  chtublem  23207  sumdchr  23268  bposlem6  23285  lgsval  23296  dchrvmasumiflem2  23408  padicabvcxp  23538  prodss  28642  dfrdg3  28792  ftc1anclem2  29655  ftc1anclem5  29658  ftc1anclem7  29660
  Copyright terms: Public domain W3C validator