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

Theorem ifeq1da 3818
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 3806 . 2  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)
3 iffalse 3798 . . . 4  |-  ( -. 
ps  ->  if ( ps ,  A ,  C
)  =  C )
4 iffalse 3798 . . . 4  |-  ( -. 
ps  ->  if ( ps ,  B ,  C
)  =  C )
53, 4eqtr4d 2477 . . 3  |-  ( -. 
ps  ->  if ( ps ,  A ,  C
)  =  if ( ps ,  B ,  C ) )
65adantl 466 . 2  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)
72, 6pm2.61dan 789 1  |-  ( ph  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    = wceq 1369   ifcif 3790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-rab 2723  df-v 2973  df-un 3332  df-if 3791
This theorem is referenced by:  cantnflem1d  7895  cantnflem1  7896  cantnflem1dOLD  7918  cantnflem1OLD  7919  dfac12lem1  8311  xrmaxeq  11150  xrmineq  11151  rexmul  11233  max0add  12798  fsumser  13206  ramcl  14089  dmdprdsplitlem  16533  dmdprdsplitlemOLD  16534  coe1pwmul  17731  mulmarep1gsum1  18383  maducoeval2  18445  madugsum  18448  madurid  18449  ptcld  19185  copco  20589  ibllem  21241  itgvallem3  21262  iblposlem  21268  iblss2  21282  iblmulc2  21307  cnplimc  21361  limcco  21367  dvexp3  21449  dchrinvcl  22591  lgsval2lem  22644  lgsval4lem  22645  lgsneg  22657  lgsmod  22659  lgsdilem2  22669  rpvmasum2  22760  ftc1anclem6  28470  ftc1anclem8  28472
  Copyright terms: Public domain W3C validator