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

Theorem ifeq2da 3970
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 3945 . . . 4  |-  ( ps 
->  if ( ps ,  C ,  A )  =  C )
2 iftrue 3945 . . . 4  |-  ( ps 
->  if ( ps ,  C ,  B )  =  C )
31, 2eqtr4d 2511 . . 3  |-  ( ps 
->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B )
)
43adantl 466 . 2  |-  ( (
ph  /\  ps )  ->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B )
)
5 ifeq2da.1 . . 3  |-  ( (
ph  /\  -.  ps )  ->  A  =  B )
65ifeq2d 3958 . 2  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B )
)
74, 6pm2.61dan 789 1  |-  ( ph  ->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    = wceq 1379   ifcif 3939
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 2823  df-v 3115  df-un 3481  df-if 3940
This theorem is referenced by:  dfac12lem1  8519  ttukeylem3  8887  xmulcom  11454  xmulneg1  11457  subgmulg  16007  1marepvmarrepid  18841  copco  21250  pcopt2  21255  limcdif  22012  limcmpt  22019  limcres  22022  limccnp  22027  radcnv0  22542  leibpi  22998  efrlim  23024  dchrvmasumiflem2  23412  rpvmasum2  23422  padicabvf  23541  padicabvcxp  23542  itg2addnclem  29641
  Copyright terms: Public domain W3C validator