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

Theorem ifeq1da 3679
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 3668 . 2  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)
3 iffalse 3661 . . . 4  |-  ( -. 
ps  ->  if ( ps ,  A ,  C
)  =  C )
4 iffalse 3661 . . . 4  |-  ( -. 
ps  ->  if ( ps ,  B ,  C
)  =  C )
53, 4eqtr4d 2401 . . 3  |-  ( -. 
ps  ->  if ( ps ,  A ,  C
)  =  if ( ps ,  B ,  C ) )
65adantl 452 . 2  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)
72, 6pm2.61dan 766 1  |-  ( ph  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358    = wceq 1647   ifcif 3654
This theorem is referenced by:  riotabidva  6463  cantnflem1d  7537  cantnflem1  7538  dfac12lem1  7916  xrmaxeq  10660  xrmineq  10661  rexmul  10743  max0add  12002  fsumser  12411  ramcl  13284  dmdprdsplitlem  15482  coe1pwmul  16565  ptcld  17524  copco  18731  ibllem  19334  itgvallem3  19355  iblposlem  19361  iblss2  19375  iblmulc2  19400  cnplimc  19452  limcco  19458  dvexp3  19540  dchrinvcl  20715  lgsval2lem  20768  lgsval4lem  20769  lgsneg  20781  lgsmod  20783  lgsdilem2  20793  rpvmasum2  20884  ifeq1daOLD  25969
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-rab 2637  df-v 2875  df-un 3243  df-if 3655
  Copyright terms: Public domain W3C validator