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

Theorem ifeq1da 3756
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 3745 . 2  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)
3 iffalse 3738 . . . 4  |-  ( -. 
ps  ->  if ( ps ,  A ,  C
)  =  C )
4 iffalse 3738 . . . 4  |-  ( -. 
ps  ->  if ( ps ,  B ,  C
)  =  C )
53, 4eqtr4d 2470 . . 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 1652   ifcif 3731
This theorem is referenced by:  cantnflem1d  7636  cantnflem1  7637  dfac12lem1  8015  xrmaxeq  10759  xrmineq  10760  rexmul  10842  max0add  12107  fsumser  12516  ramcl  13389  dmdprdsplitlem  15587  coe1pwmul  16663  ptcld  17637  copco  19035  ibllem  19648  itgvallem3  19669  iblposlem  19675  iblss2  19689  iblmulc2  19714  cnplimc  19766  limcco  19772  dvexp3  19854  dchrinvcl  21029  lgsval2lem  21082  lgsval4lem  21083  lgsneg  21095  lgsmod  21097  lgsdilem2  21107  rpvmasum2  21198  ftc1anclem2  26271  ftc1anclem6  26275  ftc1anclem8  26277
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-un 3317  df-if 3732
  Copyright terms: Public domain W3C validator