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

Theorem ineq12d 3503
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 3497 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )
41, 2, 3syl2anc 643 1  |-  ( ph  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    i^i cin 3279
This theorem is referenced by:  csbing  3508  funprg  5459  funtpg  5460  offval  6271  ofrfval  6272  oev2  6726  isf32lem7  8195  ressval  13471  invffval  13938  invfval  13939  oppcinv  13956  isps  14589  dmdprd  15514  dprddisj  15522  dprdf1o  15545  dmdprdsplit2lem  15558  dmdprdpr  15562  pgpfaclem1  15594  isunit  15717  dfrhm2  15776  isrhm  15779  2idlval  16259  aspval  16342  ressmplbas2  16473  pjfval  16888  iscon  17429  consuba  17436  ptbasin  17562  ptclsg  17600  qtopval  17680  rnelfmlem  17937  trust  18212  isnmhm  18733  uniioombllem2a  19427  dyaddisjlem  19440  dyaddisj  19441  i1faddlem  19538  i1fmullem  19539  limcflf  19721  ispth  21521  1pthonlem2  21543  2pthlem2  21549  constr2pth  21554  constr3pthlem3  21597  chocin  22950  cmbr3  23063  pjoml3  23067  fh1  23073  xppreima2  24013  hauseqcn  24246  cndprobval  24644  ballotlemfrc  24737  itg2addnclem2  26156  clsun  26221  heiborlem4  26413  heiborlem6  26415  heiborlem10  26419  aomclem8  27027  usgra2pthspth  28035  frisusgranb  28101  2spotdisj  28164  bnj1421  29117  pmodl42N  30333  polfvalN  30386  poldmj1N  30410  pmapj2N  30411  pnonsingN  30415  psubclinN  30430  poml4N  30435  osumcllem9N  30446  trnfsetN  30637  diainN  31540  djaffvalN  31616  djafvalN  31617  djajN  31620  dihmeetcl  31828  dihmeet2  31829  dochnoncon  31874  djhffval  31879  djhfval  31880  djhlj  31884  dochdmm1  31893  lclkrlem2g  31996  lclkrlem2v  32011  lcfrlem21  32046  lcfrlem24  32049  mapdunirnN  32133  baerlem5amN  32199  baerlem5bmN  32200  baerlem5abmN  32201  mapdheq4lem  32214  mapdh6lem1N  32216  mapdh6lem2N  32217  hdmap1l6lem1  32291  hdmap1l6lem2  32292
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287
  Copyright terms: Public domain W3C validator