Theorem ineq1d 2213

Description: Equality deduction for intersection of two classes.

Hypothesis

Ref	Expression
ineq1d.1	|- (ph -> A = B)

Assertion

Ref	Expression
ineq1d	|- (ph -> (A i^i C) = (B i^i C))

Proof of Theorem ineq1d

Step	Hyp	Ref	Expression
1		ineq1d.1	. 2 |- (ph -> A = B)
2		ineq1 2207	. 2 |- (A = B -> (A i^i C) = (B i^i C))
3	1, 2	syl 10	1 |- (ph -> (A i^i C) = (B i^i C))

Syntax hints:   -> wi 3   = wceq 955   i^i cin 2043

This theorem is referenced by:  ineq12d 2215  fnresdisj 3593  funimadisj 3602  fiint 4543  kmlem12 4759  limsupvalt 6474  subtop 7606  indistop 7608  bcthlem15 7975  chdmj2t 9408  cmcmlem 9491  pjoml2t 9511  fh2t 9519  mdbrt 10177  mdit 10178  mdbr3 10180  mdbr4 10181  dmdmdt 10183  dmdbr3 10188  dmdbr4 10189  dmdi4 10190  dmdbr5 10191  mddmd 10192  mdsl1 10204  cvmd 10207  mdslmd1lem1 10208  mdslmd1lem2 10209  mdslmd1lem3 10210  mdslmd1lem4 10211  mdslmd1 10212  mdslmd3 10215  csmdsym 10217  mdexch 10218  atoml 10265  atabs 10284  sumdmdlem2 10302  dmdbr5at 10305

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-v 1809  df-in 2048

Copyright terms: Public domain