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

Theorem ineq12d 3556
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 3550 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )
41, 2, 3syl2anc 661 1  |-  ( ph  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    i^i cin 3330
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-v 2977  df-in 3338
This theorem is referenced by:  csbin  3715  csbingOLD  3716  funprg  5470  funtpg  5471  offval  6330  ofrfval  6331  oev2  6966  isf32lem7  8531  ressval  14228  invffval  14699  invfval  14700  oppcinv  14717  isps  15375  dmdprd  16483  dprddisj  16496  dprdf1o  16532  dmdprdsplit2lem  16547  dmdprdpr  16551  pgpfaclem1  16585  isunit  16752  dfrhm2  16811  isrhm  16814  2idlval  17318  aspval  17402  ressmplbas2  17537  pjfval  18134  iscon  19020  consuba  19027  ptbasin  19153  ptclsg  19191  qtopval  19271  rnelfmlem  19528  trust  19807  isnmhm  20328  uniioombllem2a  21065  dyaddisjlem  21078  dyaddisj  21079  i1faddlem  21174  i1fmullem  21175  limcflf  21359  ispth  23470  1pthonlem2  23492  2pthlem2  23498  constr2pth  23503  constr3pthlem3  23546  chocin  24901  cmbr3  25014  pjoml3  25018  fh1  25024  xppreima2  25968  hauseqcn  26328  prsssdm  26350  ordtrestNEW  26354  ordtrest2NEW  26356  cndprobval  26819  ballotlemfrc  26912  predeq123  27629  itg2addnclem2  28447  clsun  28526  heiborlem4  28716  heiborlem6  28718  heiborlem10  28722  aomclem8  29417  usgra2pthspth  30298  frisusgranb  30592  2spotdisj  30657  bnj1421  32036  pmodl42N  33498  polfvalN  33551  poldmj1N  33575  pmapj2N  33576  pnonsingN  33580  psubclinN  33595  poml4N  33600  osumcllem9N  33611  trnfsetN  33802  diainN  34705  djaffvalN  34781  djafvalN  34782  djajN  34785  dihmeetcl  34993  dihmeet2  34994  dochnoncon  35039  djhffval  35044  djhfval  35045  djhlj  35049  dochdmm1  35058  lclkrlem2g  35161  lclkrlem2v  35176  lcfrlem21  35211  lcfrlem24  35214  mapdunirnN  35298  baerlem5amN  35364  baerlem5bmN  35365  baerlem5abmN  35366  mapdheq4lem  35379  mapdh6lem1N  35381  mapdh6lem2N  35382  hdmap1l6lem1  35456  hdmap1l6lem2  35457
  Copyright terms: Public domain W3C validator