Theorem ineq12 2209

Description: Equality theorem for intersection of two classes.

Assertion

Ref	Expression
ineq12	|- ((A = B /\ C = D) -> (A i^i C) = (B i^i D))

Proof of Theorem ineq12

Step	Hyp	Ref	Expression
1		ineq1 2207	. 2 |- (A = B -> (A i^i C) = (B i^i C))
2		ineq2 2208	. 2 |- (C = D -> (B i^i C) = (B i^i D))
3	1, 2	sylan9eq 1525	1 |- ((A = B /\ C = D) -> (A i^i C) = (B i^i D))

Syntax hints:   -> wi 3   /\ wa 223   = wceq 955   i^i cin 2043

This theorem is referenced by:  ineq12i 2212  ineqan12d 2216  ssin 2229  fnun 3590  endisj 4426  sbthlem8 4443  abfii4 4547  pm54.43 4555  kmlem9 4756  infxpidmlem11 7522  subbas 7604  subtop 7606  indistop 7608  retopbas 7615  ficli 10426  oefil2 10500  infi 10507  rcfpfillem4 10514

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