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

Theorem ineq12d 3615
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 3609 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )
41, 2, 3syl2anc 659 1  |-  ( ph  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1399    i^i cin 3388
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-v 3036  df-in 3396
This theorem is referenced by:  csbin  3777  funprg  5545  funtpg  5546  offval  6446  ofrfval  6447  oev2  7091  isf32lem7  8652  ressval  14688  invffval  15164  invfval  15165  dfiso2  15178  isofn  15181  oppcinv  15186  zerooval  15395  isps  15949  dmdprd  17142  dprddisj  17155  dprdf1o  17192  dmdprdsplit2lem  17207  dmdprdpr  17211  pgpfaclem1  17245  isunit  17419  dfrhm2  17479  isrhm  17483  2idlval  17994  aspval  18090  ressmplbas2  18230  pjfval  18828  iscon  19999  consuba  20006  ptbasin  20163  ptclsg  20201  qtopval  20281  rnelfmlem  20538  trust  20817  isnmhm  21338  uniioombllem2a  22076  dyaddisjlem  22089  dyaddisj  22090  i1faddlem  22185  i1fmullem  22186  limcflf  22370  ispth  24691  1pthonlem2  24713  2pthlem2  24719  constr2pth  24724  constr3pthlem3  24778  frisusgranb  25118  2spotdisj  25182  chocin  26530  cmbr3  26643  pjoml3  26647  fh1  26653  xppreima2  27628  hauseqcn  28031  prsssdm  28053  ordtrestNEW  28057  ordtrest2NEW  28059  cndprobval  28555  ballotlemfrc  28648  msrval  29087  msrf  29091  ismfs  29098  predeq123  29410  itg2addnclem2  30233  clsun  30312  heiborlem4  30476  heiborlem6  30478  heiborlem10  30482  aomclem8  31173  dvsinax  31874  dvcosax  31889  usgra2pthspth  32669  rhmval  32925  csbingOLD  33965  bnj1421  34445  pmodl42N  35988  polfvalN  36041  poldmj1N  36065  pmapj2N  36066  pnonsingN  36070  psubclinN  36085  poml4N  36090  osumcllem9N  36101  trnfsetN  36293  diainN  37197  djaffvalN  37273  djafvalN  37274  djajN  37277  dihmeetcl  37485  dihmeet2  37486  dochnoncon  37531  djhffval  37536  djhfval  37537  djhlj  37541  dochdmm1  37550  lclkrlem2g  37653  lclkrlem2v  37668  lcfrlem21  37703  lcfrlem24  37706  mapdunirnN  37790  baerlem5amN  37856  baerlem5bmN  37857  baerlem5abmN  37858  mapdheq4lem  37871  mapdh6lem1N  37873  mapdh6lem2N  37874  hdmap1l6lem1  37948  hdmap1l6lem2  37949
  Copyright terms: Public domain W3C validator