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

Theorem ineq12d 3686
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 3680 . 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 1383    i^i cin 3460
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-in 3468
This theorem is referenced by:  csbin  3846  csbingOLD  3847  funprg  5627  funtpg  5628  offval  6532  ofrfval  6533  oev2  7175  isf32lem7  8742  ressval  14561  invffval  15029  invfval  15030  oppcinv  15047  isps  15706  dmdprd  16903  dprddisj  16916  dprdf1o  16953  dmdprdsplit2lem  16968  dmdprdpr  16972  pgpfaclem1  17006  isunit  17180  dfrhm2  17240  isrhm  17244  2idlval  17755  aspval  17851  ressmplbas2  17991  pjfval  18610  iscon  19787  consuba  19794  ptbasin  19951  ptclsg  19989  qtopval  20069  rnelfmlem  20326  trust  20605  isnmhm  21126  uniioombllem2a  21864  dyaddisjlem  21877  dyaddisj  21878  i1faddlem  21973  i1fmullem  21974  limcflf  22158  ispth  24442  1pthonlem2  24464  2pthlem2  24470  constr2pth  24475  constr3pthlem3  24529  frisusgranb  24869  2spotdisj  24933  chocin  26285  cmbr3  26398  pjoml3  26402  fh1  26408  xppreima2  27360  hauseqcn  27750  prsssdm  27772  ordtrestNEW  27776  ordtrest2NEW  27778  cndprobval  28245  ballotlemfrc  28338  msrval  28771  msrf  28775  ismfs  28782  predeq123  29220  itg2addnclem2  30042  clsun  30121  heiborlem4  30285  heiborlem6  30287  heiborlem10  30291  aomclem8  30982  dvsinax  31612  dvcosax  31627  usgra2pthspth  32189  rhmval  32432  bnj1421  33826  pmodl42N  35309  polfvalN  35362  poldmj1N  35386  pmapj2N  35387  pnonsingN  35391  psubclinN  35406  poml4N  35411  osumcllem9N  35422  trnfsetN  35614  diainN  36518  djaffvalN  36594  djafvalN  36595  djajN  36598  dihmeetcl  36806  dihmeet2  36807  dochnoncon  36852  djhffval  36857  djhfval  36858  djhlj  36862  dochdmm1  36871  lclkrlem2g  36974  lclkrlem2v  36989  lcfrlem21  37024  lcfrlem24  37027  mapdunirnN  37111  baerlem5amN  37177  baerlem5bmN  37178  baerlem5abmN  37179  mapdheq4lem  37192  mapdh6lem1N  37194  mapdh6lem2N  37195  hdmap1l6lem1  37269  hdmap1l6lem2  37270
  Copyright terms: Public domain W3C validator