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

Theorem ifeq2da 3591
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 3571 . . . 4  |-  ( ps 
->  if ( ps ,  C ,  A )  =  C )
2 iftrue 3571 . . . 4  |-  ( ps 
->  if ( ps ,  C ,  B )  =  C )
31, 2eqtr4d 2318 . . 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 3580 . 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 1623   ifcif 3565
This theorem is referenced by:  dfac12lem1  7769  ttukeylem3  8138  xmulcom  10586  xmulneg1  10589  subgmulg  14635  copco  18516  pcopt2  18521  limcdif  19226  limcmpt  19233  limcres  19236  limccnp  19241  radcnv0  19792  leibpi  20238  efrlim  20264  dchrvmasumiflem2  20651  rpvmasum2  20661  padicabvf  20780  padicabvcxp  20781  ifeq2daOLD  26378
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-un 3157  df-if 3566
  Copyright terms: Public domain W3C validator