Theorem indir 3745

Description: Distributive law for intersection over union. Theorem 28 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.)

Assertion

Ref	Expression
indir

Proof of Theorem indir

Step	Hyp	Ref	Expression
1		indi 3743	. 2
2		incom 3690	. 2
3		incom 3690	. . 3
4		incom 3690	. . 3
5	3, 4	uneq12i 3655	. 2
6	1, 2, 5	3eqtr4i 2496	1

Syntax hints:  =wceq 1395  u.cun 3473  i^icin 3474

This theorem is referenced by:  difundir  3750  undisj1  3878  disjpr2  4092  resundir  5293  cdaassen  8583  fin23lem26  8726  fpwwe2lem13  9041  neitr  19681  fiuncmp  19904  consuba  19921  trfil2  20388  tsmsresOLD  20645  tsmsres  20646  trust  20732  restmetu  21090  volun  21955  uniioombllem3  21994  itgsplitioo  22244  ppiprm  23425  chtprm  23427  chtdif  23432  ppidif  23437  ballotlemfp1  28430  ballotlemgun  28463  mrsubvrs  28882  mthmpps  28942  predun  29270  fixun  29559  mbfposadd  30062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-in 3482