Theorem andi 1010

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 868	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
2		olc 869	. . 3 ⊢ ((𝜑 ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
3	1, 2	jaodan 960	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
4		orc 868	. . . 4 ⊢ (𝜓 → (𝜓 ∨ 𝜒))
5	4	anim2i 618	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
6		olc 869	. . . 4 ⊢ (𝜒 → (𝜓 ∨ 𝜒))
7	6	anim2i 618	. . 3 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
8	5, 7	jaoi 858	. 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
9	3, 8	impbii 209	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∨ wo 848

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 207  df-an 396  df-or 849

This theorem is referenced by:  andir  1011  anddi  1013  cadan  1611  indi  4238  unrab  4269  uniun  4888  unopab  5180  xpundi  5701  difxp  6130  coundir  6214  imadif  6584  unpreima  7017  soseq  8111  tpostpos  8198  elznn0nn  12514  faclbnd4lem4  14231  opsrtoslem1  22022  mbfmax  25618  fta1glem2  26142  ofmulrt  26257  lgsquadlem3  27361  nogesgn1o  27653  nosep1o  27661  noinfbnd2lem1  27710  difrab2  32583  ordtconnlem1  34101  ballotlemodife  34675  subfacp1lem6  35398  satf0op  35590  lineunray  36360  bj-axseprep  37316  wl-ifpimpr  37715  wl-df2-3mintru2  37734  poimirlem30  37895  itg2addnclem2  37917  sticksstones22  42532  lzunuz  43119  diophun  43124  rmydioph  43365  fzunt  43805  fzuntd  43806  fzunt1d  43807  fzuntgd  43808  rp-isfinite6  43868  relexpxpmin  44067  andi3or  44374  clsk1indlem3  44393  simpcntrab  47222  zeoALTV  48024