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

Theorem ifeq2da 3757
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 3737 . . . 4  |-  ( ps 
->  if ( ps ,  C ,  A )  =  C )
2 iftrue 3737 . . . 4  |-  ( ps 
->  if ( ps ,  C ,  B )  =  C )
31, 2eqtr4d 2470 . . 3  |-  ( ps 
->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B )
)
43adantl 453 . 2  |-  ( (
ph  /\  ps )  ->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B )
)
5 ifeq2da.1 . . 3  |-  ( (
ph  /\  -.  ps )  ->  A  =  B )
65ifeq2d 3746 . 2  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B )
)
74, 6pm2.61dan 767 1  |-  ( ph  ->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 359    = wceq 1652   ifcif 3731
This theorem is referenced by:  dfac12lem1  8015  ttukeylem3  8383  xmulcom  10837  xmulneg1  10840  subgmulg  14950  copco  19035  pcopt2  19040  limcdif  19755  limcmpt  19762  limcres  19765  limccnp  19770  radcnv0  20324  leibpi  20774  efrlim  20800  dchrvmasumiflem2  21188  rpvmasum2  21198  padicabvf  21317  padicabvcxp  21318  itg2addnclem  26246
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-un 3317  df-if 3732
  Copyright terms: Public domain W3C validator