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

Theorem ineq12d 3541
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 3535 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )
41, 2, 3syl2anc 654 1  |-  ( ph  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362    i^i cin 3315
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-in 3323
This theorem is referenced by:  csbin  3700  csbingOLD  3701  funprg  5455  funtpg  5456  offval  6316  ofrfval  6317  oev2  6951  isf32lem7  8516  ressval  14208  invffval  14679  invfval  14680  oppcinv  14697  isps  15355  dmdprd  16454  dprddisj  16467  dprdf1o  16503  dmdprdsplit2lem  16518  dmdprdpr  16522  pgpfaclem1  16556  isunit  16683  dfrhm2  16742  isrhm  16745  2idlval  17237  aspval  17321  ressmplbas2  17468  pjfval  17973  iscon  18859  consuba  18866  ptbasin  18992  ptclsg  19030  qtopval  19110  rnelfmlem  19367  trust  19646  isnmhm  20167  uniioombllem2a  20904  dyaddisjlem  20917  dyaddisj  20918  i1faddlem  21013  i1fmullem  21014  limcflf  21198  ispth  23290  1pthonlem2  23312  2pthlem2  23318  constr2pth  23323  constr3pthlem3  23366  chocin  24721  cmbr3  24834  pjoml3  24838  fh1  24844  xppreima2  25789  hauseqcn  26179  prsssdm  26201  ordtrestNEW  26205  ordtrest2NEW  26207  cndprobval  26664  ballotlemfrc  26757  predeq123  27473  itg2addnclem2  28288  clsun  28367  heiborlem4  28557  heiborlem6  28559  heiborlem10  28563  aomclem8  29259  usgra2pthspth  30141  frisusgranb  30435  2spotdisj  30500  bnj1421  31735  pmodl42N  33068  polfvalN  33121  poldmj1N  33145  pmapj2N  33146  pnonsingN  33150  psubclinN  33165  poml4N  33170  osumcllem9N  33181  trnfsetN  33372  diainN  34275  djaffvalN  34351  djafvalN  34352  djajN  34355  dihmeetcl  34563  dihmeet2  34564  dochnoncon  34609  djhffval  34614  djhfval  34615  djhlj  34619  dochdmm1  34628  lclkrlem2g  34731  lclkrlem2v  34746  lcfrlem21  34781  lcfrlem24  34784  mapdunirnN  34868  baerlem5amN  34934  baerlem5bmN  34935  baerlem5abmN  34936  mapdheq4lem  34949  mapdh6lem1N  34951  mapdh6lem2N  34952  hdmap1l6lem1  35026  hdmap1l6lem2  35027
  Copyright terms: Public domain W3C validator