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

Theorem ineq12d 3384
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 3378 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )
41, 2, 3syl2anc 642 1  |-  ( ph  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    i^i cin 3164
This theorem is referenced by:  csbing  3389  funprg  5317  offval  6101  ofrfval  6102  oev2  6538  isf32lem7  8001  ressval  13211  invffval  13676  invfval  13677  oppcinv  13694  isps  14327  dmdprd  15252  dprddisj  15260  dprdf1o  15283  dmdprdsplit2lem  15296  dmdprdpr  15300  pgpfaclem1  15332  isunit  15455  dfrhm2  15514  isrhm  15517  2idlval  16001  aspval  16084  ressmplbas2  16215  pjfval  16622  iscon  17155  consuba  17162  ptbasin  17288  ptclsg  17325  qtopval  17402  rnelfmlem  17663  isnmhm  18271  uniioombllem2a  18953  dyaddisjlem  18966  dyaddisj  18967  i1faddlem  19064  i1fmullem  19065  limcflf  19247  chocin  22090  cmbr3  22203  pjoml3  22207  fh1  22213  ballotlemfrc  23101  xppreima2  23227  cndprobval  23651  itg2addnclem2  25004  clsun  26349  heiborlem4  26641  heiborlem6  26643  heiborlem10  26647  aomclem8  27262  ispth  28354  constr3pthlem3  28403  bnj1421  29388  pmodl42N  30662  polfvalN  30715  poldmj1N  30739  pmapj2N  30740  pnonsingN  30744  psubclinN  30759  poml4N  30764  osumcllem9N  30775  trnfsetN  30966  diainN  31869  djaffvalN  31945  djafvalN  31946  djajN  31949  dihmeetcl  32157  dihmeet2  32158  dochnoncon  32203  djhffval  32208  djhfval  32209  djhlj  32213  dochdmm1  32222  lclkrlem2g  32325  lclkrlem2v  32340  lcfrlem21  32375  lcfrlem24  32378  mapdunirnN  32462  baerlem5amN  32528  baerlem5bmN  32529  baerlem5abmN  32530  mapdheq4lem  32543  mapdh6lem1N  32545  mapdh6lem2N  32546  hdmap1l6lem1  32620  hdmap1l6lem2  32621
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172
  Copyright terms: Public domain W3C validator