Theorem ineq12 2212

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 2210	. 2 |- (A = B -> (A i^i C) = (B i^i C))
2		ineq2 2211	. 2 |- (C = D -> (B i^i C) = (B i^i D))
3	1, 2	sylan9eq 1527	1 |- ((A = B /\ C = D) -> (A i^i C) = (B i^i D))

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

This theorem is referenced by:  ineq12i 2215  ineqan12d 2219  ssin 2232  fnun 3594  endisj 4437  sbthlem8 4454  abfii4OLD 4564  pm54.43 4572  kmlem9 4773  infxpidmlem11 7562  subbasOLD 7644  subtop 7646  indistop 7648  retopbas 7655  ficli 10472  ficliOLD 10473  oefil2 10567  infi 10578  infiOLD 10579  rcfpfillem4 10591  rcfpfillem4OLD 10592

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-in 2051

Copyright terms: Public domain