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

Theorem ineq12d 3371
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 3365 . 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 1623    i^i cin 3151
This theorem is referenced by:  csbing  3376  funprg  5301  offval  6085  ofrfval  6086  oev2  6522  isf32lem7  7985  ressval  13195  invffval  13660  invfval  13661  oppcinv  13678  isps  14311  dmdprd  15236  dprddisj  15244  dprdf1o  15267  dmdprdsplit2lem  15280  dmdprdpr  15284  pgpfaclem1  15316  isunit  15439  dfrhm2  15498  isrhm  15501  2idlval  15985  aspval  16068  ressmplbas2  16199  pjfval  16606  iscon  17139  consuba  17146  ptbasin  17272  ptclsg  17309  qtopval  17386  rnelfmlem  17647  isnmhm  18255  uniioombllem2a  18937  dyaddisjlem  18950  dyaddisj  18951  i1faddlem  19048  i1fmullem  19049  limcflf  19231  chocin  22074  cmbr3  22187  pjoml3  22191  fh1  22197  ballotlemfrc  23085  xppreima2  23212  cndprobval  23636  clsun  26246  heiborlem4  26538  heiborlem6  26540  heiborlem10  26544  aomclem8  27159  bnj1421  29072  pmodl42N  30040  polfvalN  30093  poldmj1N  30117  pmapj2N  30118  pnonsingN  30122  psubclinN  30137  poml4N  30142  osumcllem9N  30153  trnfsetN  30344  diainN  31247  djaffvalN  31323  djafvalN  31324  djajN  31327  dihmeetcl  31535  dihmeet2  31536  dochnoncon  31581  djhffval  31586  djhfval  31587  djhlj  31591  dochdmm1  31600  lclkrlem2g  31703  lclkrlem2v  31718  lcfrlem21  31753  lcfrlem24  31756  mapdunirnN  31840  baerlem5amN  31906  baerlem5bmN  31907  baerlem5abmN  31908  mapdheq4lem  31921  mapdh6lem1N  31923  mapdh6lem2N  31924  hdmap1l6lem1  31998  hdmap1l6lem2  31999
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159
  Copyright terms: Public domain W3C validator