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

Theorem ifeq2da 3915
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 3890 . . . 4  |-  ( ps 
->  if ( ps ,  C ,  A )  =  C )
2 iftrue 3890 . . . 4  |-  ( ps 
->  if ( ps ,  C ,  B )  =  C )
31, 2eqtr4d 2446 . . 3  |-  ( ps 
->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B )
)
43adantl 464 . 2  |-  ( (
ph  /\  ps )  ->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B )
)
5 ifeq2da.1 . . 3  |-  ( (
ph  /\  -.  ps )  ->  A  =  B )
65ifeq2d 3903 . 2  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B )
)
74, 6pm2.61dan 792 1  |-  ( ph  ->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 367    = wceq 1405   ifcif 3884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rab 2762  df-v 3060  df-un 3418  df-if 3885
This theorem is referenced by:  dfac12lem1  8554  ttukeylem3  8922  xmulcom  11510  xmulneg1  11513  subgmulg  16537  1marepvmarrepid  19367  copco  21808  pcopt2  21813  limcdif  22570  limcmpt  22577  limcres  22580  limccnp  22585  radcnv0  23101  leibpi  23596  efrlim  23623  dchrvmasumiflem2  24066  rpvmasum2  24076  padicabvf  24195  padicabvcxp  24196  itg2addnclem  31419  fourierdlem73  37311  fourierdlem76  37314  fourierdlem89  37327  fourierdlem91  37329
  Copyright terms: Public domain W3C validator