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

Theorem ineq12d 3543
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 3537 . 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 1652    i^i cin 3319
This theorem is referenced by:  csbing  3548  funprg  5500  funtpg  5501  offval  6312  ofrfval  6313  oev2  6767  isf32lem7  8239  ressval  13516  invffval  13983  invfval  13984  oppcinv  14001  isps  14634  dmdprd  15559  dprddisj  15567  dprdf1o  15590  dmdprdsplit2lem  15603  dmdprdpr  15607  pgpfaclem1  15639  isunit  15762  dfrhm2  15821  isrhm  15824  2idlval  16304  aspval  16387  ressmplbas2  16518  pjfval  16933  iscon  17476  consuba  17483  ptbasin  17609  ptclsg  17647  qtopval  17727  rnelfmlem  17984  trust  18259  isnmhm  18780  uniioombllem2a  19474  dyaddisjlem  19487  dyaddisj  19488  i1faddlem  19585  i1fmullem  19586  limcflf  19768  ispth  21568  1pthonlem2  21590  2pthlem2  21596  constr2pth  21601  constr3pthlem3  21644  chocin  22997  cmbr3  23110  pjoml3  23114  fh1  23120  xppreima2  24060  hauseqcn  24293  cndprobval  24691  ballotlemfrc  24784  predeq123  25440  itg2addnclem2  26257  clsun  26331  heiborlem4  26523  heiborlem6  26525  heiborlem10  26529  aomclem8  27136  usgra2pthspth  28305  frisusgranb  28387  2spotdisj  28450  bnj1421  29411  pmodl42N  30648  polfvalN  30701  poldmj1N  30725  pmapj2N  30726  pnonsingN  30730  psubclinN  30745  poml4N  30750  osumcllem9N  30761  trnfsetN  30952  diainN  31855  djaffvalN  31931  djafvalN  31932  djajN  31935  dihmeetcl  32143  dihmeet2  32144  dochnoncon  32189  djhffval  32194  djhfval  32195  djhlj  32199  dochdmm1  32208  lclkrlem2g  32311  lclkrlem2v  32326  lcfrlem21  32361  lcfrlem24  32364  mapdunirnN  32448  baerlem5amN  32514  baerlem5bmN  32515  baerlem5abmN  32516  mapdheq4lem  32529  mapdh6lem1N  32531  mapdh6lem2N  32532  hdmap1l6lem1  32606  hdmap1l6lem2  32607
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-in 3327
  Copyright terms: Public domain W3C validator