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

Theorem ifeq2da 3604
Description: Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.)
Hypothesis
Ref Expression
ifeq2da.1  |-  ( (
ph  /\  -.  ps )  ->  A  =  B )
Assertion
Ref Expression
ifeq2da  |-  ( ph  ->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B )
)

Proof of Theorem ifeq2da
StepHypRef Expression
1 iftrue 3584 . . . 4  |-  ( ps 
->  if ( ps ,  C ,  A )  =  C )
2 iftrue 3584 . . . 4  |-  ( ps 
->  if ( ps ,  C ,  B )  =  C )
31, 2eqtr4d 2331 . . 3  |-  ( ps 
->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B )
)
43adantl 452 . 2  |-  ( (
ph  /\  ps )  ->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B )
)
5 ifeq2da.1 . . 3  |-  ( (
ph  /\  -.  ps )  ->  A  =  B )
65ifeq2d 3593 . 2  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B )
)
74, 6pm2.61dan 766 1  |-  ( ph  ->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358    = wceq 1632   ifcif 3578
This theorem is referenced by:  dfac12lem1  7785  ttukeylem3  8154  xmulcom  10602  xmulneg1  10605  subgmulg  14651  copco  18532  pcopt2  18537  limcdif  19242  limcmpt  19249  limcres  19252  limccnp  19257  radcnv0  19808  leibpi  20254  efrlim  20280  dchrvmasumiflem2  20667  rpvmasum2  20677  padicabvf  20796  padicabvcxp  20797  itg2addnclem  25003  ifeq2daOLD  26481
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-un 3170  df-if 3579
  Copyright terms: Public domain W3C validator