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

Theorem ifeq1da 3766
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 3755 . 2  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)
3 iffalse 3748 . . . 4  |-  ( -. 
ps  ->  if ( ps ,  A ,  C
)  =  C )
4 iffalse 3748 . . . 4  |-  ( -. 
ps  ->  if ( ps ,  B ,  C
)  =  C )
53, 4eqtr4d 2473 . . 3  |-  ( -. 
ps  ->  if ( ps ,  A ,  C
)  =  if ( ps ,  B ,  C ) )
65adantl 454 . 2  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)
72, 6pm2.61dan 768 1  |-  ( ph  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 360    = wceq 1653   ifcif 3741
This theorem is referenced by:  cantnflem1d  7647  cantnflem1  7648  dfac12lem1  8028  xrmaxeq  10772  xrmineq  10773  rexmul  10855  max0add  12120  fsumser  12529  ramcl  13402  dmdprdsplitlem  15600  coe1pwmul  16676  ptcld  17650  copco  19048  ibllem  19659  itgvallem3  19680  iblposlem  19686  iblss2  19700  iblmulc2  19725  cnplimc  19779  limcco  19785  dvexp3  19867  dchrinvcl  21042  lgsval2lem  21095  lgsval4lem  21096  lgsneg  21108  lgsmod  21110  lgsdilem2  21120  rpvmasum2  21211  ftc1anclem6  26299  ftc1anclem8  26301
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-v 2960  df-un 3327  df-if 3742
  Copyright terms: Public domain W3C validator