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

Theorem ifeq1da 3975
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 3963 . 2  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)
3 iffalse 3954 . . . 4  |-  ( -. 
ps  ->  if ( ps ,  A ,  C
)  =  C )
4 iffalse 3954 . . . 4  |-  ( -. 
ps  ->  if ( ps ,  B ,  C
)  =  C )
53, 4eqtr4d 2511 . . 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 1379   ifcif 3945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2826  df-v 3120  df-un 3486  df-if 3946
This theorem is referenced by:  cantnflem1d  8119  cantnflem1  8120  cantnflem1dOLD  8142  cantnflem1OLD  8143  dfac12lem1  8535  xrmaxeq  11392  xrmineq  11393  rexmul  11475  max0add  13123  fsumser  13532  ramcl  14423  dmdprdsplitlem  16956  dmdprdsplitlemOLD  16957  coe1pwmul  18190  scmatscmiddistr  18879  mulmarep1gsum1  18944  maducoeval2  19011  madugsum  19014  madurid  19015  ptcld  19982  copco  21386  ibllem  22039  itgvallem3  22060  iblposlem  22066  iblss2  22080  iblmulc2  22105  cnplimc  22159  limcco  22165  dvexp3  22247  dchrinvcl  23394  lgsval2lem  23447  lgsval4lem  23448  lgsneg  23460  lgsmod  23462  lgsdilem2  23472  rpvmasum2  23563  mrsubrn  28689  ftc1anclem6  30013  ftc1anclem8  30015
  Copyright terms: Public domain W3C validator