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

Theorem ineq12d 3608
Description: Equality deduction for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Hypotheses
Ref Expression
ineq1d.1  |-  ( ph  ->  A  =  B )
ineq12d.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
ineq12d  |-  ( ph  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )

Proof of Theorem ineq12d
StepHypRef Expression
1 ineq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 ineq12d.2 . 2  |-  ( ph  ->  C  =  D )
3 ineq12 3602 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )
41, 2, 3syl2anc 665 1  |-  ( ph  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    i^i cin 3378
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-v 3024  df-in 3386
This theorem is referenced by:  csbin  3772  predeq123  5343  funprg  5593  funtpg  5594  offval  6496  ofrfval  6497  oev2  7180  isf32lem7  8740  ressval  15119  invffval  15606  invfval  15607  dfiso2  15620  isofn  15623  oppcinv  15628  zerooval  15837  isps  16391  dmdprd  17573  dprddisj  17584  dprdf1o  17608  dmdprdsplit2lem  17621  dmdprdpr  17625  pgpfaclem1  17657  isunit  17828  dfrhm2  17888  isrhm  17892  2idlval  18400  aspval  18495  ressmplbas2  18622  pjfval  19211  iscon  20370  consuba  20377  ptbasin  20534  ptclsg  20572  qtopval  20652  rnelfmlem  20909  trust  21186  isnmhm  21709  uniioombllem2a  22481  dyaddisjlem  22495  dyaddisj  22496  i1faddlem  22593  i1fmullem  22594  limcflf  22778  ispth  25240  1pthonlem2  25262  2pthlem2  25268  constr2pth  25273  constr3pthlem3  25327  frisusgranb  25667  2spotdisj  25731  chocin  27090  cmbr3  27203  pjoml3  27207  fh1  27213  xppreima2  28195  hauseqcn  28653  prsssdm  28675  ordtrestNEW  28679  ordtrest2NEW  28681  cndprobval  29218  ballotlemfrc  29311  ballotlemfrcOLD  29349  bnj1421  29803  msrval  30128  msrf  30132  ismfs  30139  clsun  30933  poimirlem8  31855  itg2addnclem2  31901  heiborlem4  32053  heiborlem6  32055  heiborlem10  32059  pmodl42N  33328  polfvalN  33381  poldmj1N  33405  pmapj2N  33406  pnonsingN  33410  psubclinN  33425  poml4N  33430  osumcllem9N  33441  trnfsetN  33633  diainN  34537  djaffvalN  34613  djafvalN  34614  djajN  34617  dihmeetcl  34825  dihmeet2  34826  dochnoncon  34871  djhffval  34876  djhfval  34877  djhlj  34881  dochdmm1  34890  lclkrlem2g  34993  lclkrlem2v  35008  lcfrlem21  35043  lcfrlem24  35046  mapdunirnN  35130  baerlem5amN  35196  baerlem5bmN  35197  baerlem5abmN  35198  mapdheq4lem  35211  mapdh6lem1N  35213  mapdh6lem2N  35214  hdmap1l6lem1  35288  hdmap1l6lem2  35289  aomclem8  35832  csbingOLD  37131  disjrnmpt2  37367  dvsinax  37666  dvcosax  37681  nnfoctbdjlem  38144  usgra2pthspth  39266  rhmval  39520
  Copyright terms: Public domain W3C validator