Theorem ifeq1d 4104

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

Step	Hyp	Ref	Expression
1		ifeq1d.1	. 2 |- ( ph -> A = B )
2		ifeq1 4090	. 2 |- ( A = B -> if ( ps , A , C ) = if ( ps , B , C ) )
3	1, 2	syl 17	1 |- ( ph -> if ( ps , A , C ) = if ( ps , B , C ) )

Syntax hints:   -> wi 4   = wceq 1483   ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-un 3579  df-if 4087

This theorem is referenced by:  ifeq12d  4106  ifbieq1d  4109  ifeq1da  4116  rabsnif  4258  fsuppmptif  8305  cantnflem1  8586  sumeq2w  14422  cbvsum  14425  isumless  14577  prodss  14677  subgmulg  17608  evlslem2  19512  dmatcrng  20308  scmatscmiddistr  20314  scmatcrng  20327  marrepfval  20366  mdetr0  20411  mdetunilem8  20425  madufval  20443  madugsum  20449  minmar1fval  20452  decpmatid  20575  monmatcollpw  20584  pmatcollpwscmatlem1  20594  cnmpt2pc  22727  pcoval2  22816  pcopt  22822  itgz  23547  iblss2  23572  itgss  23578  itgcn  23609  plyeq0lem  23966  dgrcolem2  24030  plydivlem4  24051  leibpi  24669  chtublem  24936  sumdchr  24997  bposlem6  25014  lgsval  25026  dchrvmasumiflem2  25191  padicabvcxp  25321  dfrdg3  31702  matunitlindflem1  33405  ftc1anclem2  33486  ftc1anclem5  33489  ftc1anclem7  33491  hoidifhspval  40822  hoimbl  40845