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

Theorem ifeq1da 3956
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 3944 . 2  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)
3 iffalse 3935 . . . 4  |-  ( -. 
ps  ->  if ( ps ,  A ,  C
)  =  C )
4 iffalse 3935 . . . 4  |-  ( -. 
ps  ->  if ( ps ,  B ,  C
)  =  C )
53, 4eqtr4d 2487 . . 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 791 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 1383   ifcif 3926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-un 3466  df-if 3927
This theorem is referenced by:  cantnflem1d  8110  cantnflem1  8111  cantnflem1dOLD  8133  cantnflem1OLD  8134  dfac12lem1  8526  xrmaxeq  11391  xrmineq  11392  rexmul  11474  max0add  13125  sumeq2ii  13497  fsumser  13534  ramcl  14529  dmdprdsplitlem  17063  dmdprdsplitlemOLD  17064  coe1pwmul  18299  scmatscmiddistr  18988  mulmarep1gsum1  19053  maducoeval2  19120  madugsum  19123  madurid  19124  ptcld  20092  copco  21496  ibllem  22149  itgvallem3  22170  iblposlem  22176  iblss2  22190  iblmulc2  22215  cnplimc  22269  limcco  22275  dvexp3  22357  dchrinvcl  23506  lgsval2lem  23559  lgsval4lem  23560  lgsneg  23572  lgsmod  23574  lgsdilem2  23584  rpvmasum2  23675  mrsubrn  28851  ftc1anclem6  30071  ftc1anclem8  30073
  Copyright terms: Public domain W3C validator