Theorem andi 1005

Description: Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)

Assertion

Ref	Expression
andi	⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))

Proof of Theorem andi

Step	Hyp	Ref	Expression
1		orc 864	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
2		olc 865	. . 3 ⊢ ((𝜑 ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
3	1, 2	jaodan 955	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
4		orc 864	. . . 4 ⊢ (𝜓 → (𝜓 ∨ 𝜒))
5	4	anim2i 617	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
6		olc 865	. . . 4 ⊢ (𝜒 → (𝜓 ∨ 𝜒))
7	6	anim2i 617	. . 3 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
8	5, 7	jaoi 854	. 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
9	3, 8	impbii 208	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 205   ∧ wa 396   ∨ wo 844

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845

This theorem is referenced by:  andir  1006  anddi  1008  cadan  1611  indi  4207  indifdirOLD  4219  unrab  4239  uniprOLD  4858  uniun  4864  unopab  5155  xpundi  5650  difxp  6060  coundir  6145  imadif  6510  unpreima  6932  tpostpos  8049  elznn0nn  12343  faclbnd4lem4  14020  opsrtoslem1  21272  mbfmax  24823  fta1glem2  25341  ofmulrt  25452  lgsquadlem3  26540  difrab2  30853  ordtconnlem1  31882  ballotlemodife  32472  subfacp1lem6  33155  satf0op  33347  soseq  33811  nogesgn1o  33884  nosep1o  33892  noinfbnd2lem1  33941  lineunray  34457  wl-ifpimpr  35645  wl-df2-3mintru2  35664  poimirlem30  35815  itg2addnclem2  35837  sticksstones22  40132  lzunuz  40598  diophun  40603  rmydioph  40844  rp-isfinite6  41115  relexpxpmin  41306  andi3or  41613  clsk1indlem3  41634  simpcntrab  44364  zeoALTV  45100