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

Theorem ifeq1da 3732
Description: Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.)
Hypothesis
Ref Expression
ifeq1da.1  |-  ( (
ph  /\  ps )  ->  A  =  B )
Assertion
Ref Expression
ifeq1da  |-  ( ph  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)

Proof of Theorem ifeq1da
StepHypRef Expression
1 ifeq1da.1 . . 3  |-  ( (
ph  /\  ps )  ->  A  =  B )
21ifeq1d 3721 . 2  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)
3 iffalse 3714 . . . 4  |-  ( -. 
ps  ->  if ( ps ,  A ,  C
)  =  C )
4 iffalse 3714 . . . 4  |-  ( -. 
ps  ->  if ( ps ,  B ,  C
)  =  C )
53, 4eqtr4d 2447 . . 3  |-  ( -. 
ps  ->  if ( ps ,  A ,  C
)  =  if ( ps ,  B ,  C ) )
65adantl 453 . 2  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)
72, 6pm2.61dan 767 1  |-  ( ph  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 359    = wceq 1649   ifcif 3707
This theorem is referenced by:  cantnflem1d  7608  cantnflem1  7609  dfac12lem1  7987  xrmaxeq  10731  xrmineq  10732  rexmul  10814  max0add  12078  fsumser  12487  ramcl  13360  dmdprdsplitlem  15558  coe1pwmul  16634  ptcld  17606  copco  19004  ibllem  19617  itgvallem3  19638  iblposlem  19644  iblss2  19658  iblmulc2  19683  cnplimc  19735  limcco  19741  dvexp3  19823  dchrinvcl  20998  lgsval2lem  21051  lgsval4lem  21052  lgsneg  21064  lgsmod  21066  lgsdilem2  21076  rpvmasum2  21167
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-rab 2683  df-v 2926  df-un 3293  df-if 3708
  Copyright terms: Public domain W3C validator