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

Theorem ineq12d 3647
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 3641 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )
41, 2, 3syl2anc 671 1  |-  ( ph  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1455    i^i cin 3415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-in 3423
This theorem is referenced by:  csbin  3811  predeq123  5400  funprg  5650  funtpg  5651  funcnvtp  5659  offval  6565  ofrfval  6566  oev2  7251  isf32lem7  8815  ressval  15225  invffval  15712  invfval  15713  dfiso2  15726  isofn  15729  oppcinv  15734  zerooval  15943  isps  16497  dmdprd  17679  dprddisj  17690  dprdf1o  17714  dmdprdsplit2lem  17727  dmdprdpr  17731  pgpfaclem1  17763  isunit  17934  dfrhm2  17994  isrhm  17998  2idlval  18506  aspval  18601  ressmplbas2  18728  pjfval  19318  iscon  20477  consuba  20484  ptbasin  20641  ptclsg  20679  qtopval  20759  rnelfmlem  21016  trust  21293  isnmhm  21816  uniioombllem2a  22588  dyaddisjlem  22602  dyaddisj  22603  i1faddlem  22700  i1fmullem  22701  limcflf  22885  ispth  25347  1pthonlem2  25369  2pthlem2  25375  constr2pth  25380  constr3pthlem3  25434  frisusgranb  25774  2spotdisj  25838  chocin  27197  cmbr3  27310  pjoml3  27314  fh1  27320  xppreima2  28298  hauseqcn  28750  prsssdm  28772  ordtrestNEW  28776  ordtrest2NEW  28778  cndprobval  29315  ballotlemfrc  29408  ballotlemfrcOLD  29446  bnj1421  29900  msrval  30225  msrf  30229  ismfs  30236  clsun  31033  poimirlem8  31993  itg2addnclem2  32039  heiborlem4  32191  heiborlem6  32193  heiborlem10  32197  pmodl42N  33461  polfvalN  33514  poldmj1N  33538  pmapj2N  33539  pnonsingN  33543  psubclinN  33558  poml4N  33563  osumcllem9N  33574  trnfsetN  33766  diainN  34670  djaffvalN  34746  djafvalN  34747  djajN  34750  dihmeetcl  34958  dihmeet2  34959  dochnoncon  35004  djhffval  35009  djhfval  35010  djhlj  35014  dochdmm1  35023  lclkrlem2g  35126  lclkrlem2v  35141  lcfrlem21  35176  lcfrlem24  35179  mapdunirnN  35263  baerlem5amN  35329  baerlem5bmN  35330  baerlem5abmN  35331  mapdheq4lem  35344  mapdh6lem1N  35346  mapdh6lem2N  35347  hdmap1l6lem1  35421  hdmap1l6lem2  35422  aomclem8  35964  csbingOLD  37255  disjrnmpt2  37501  dvsinax  37821  dvcosax  37836  nnfoctbdjlem  38331  ewlksfval  39668  isewlk  39669  ewlkinedg  39671  isPth  39757  usgra2pthspth  39938  rhmval  40192
  Copyright terms: Public domain W3C validator