Theorem andi 1009

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

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

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 848

This theorem is referenced by:  andir  1010  anddi  1012  cadan  1610  indi  4236  unrab  4267  uniun  4886  unopab  5178  xpundi  5693  difxp  6122  coundir  6206  imadif  6576  unpreima  7008  soseq  8101  tpostpos  8188  elznn0nn  12502  faclbnd4lem4  14219  opsrtoslem1  22010  mbfmax  25606  fta1glem2  26130  ofmulrt  26245  lgsquadlem3  27349  nogesgn1o  27641  nosep1o  27649  noinfbnd2lem1  27698  difrab2  32572  ordtconnlem1  34081  ballotlemodife  34655  subfacp1lem6  35379  satf0op  35571  lineunray  36341  wl-ifpimpr  37667  wl-df2-3mintru2  37686  poimirlem30  37847  itg2addnclem2  37869  sticksstones22  42418  lzunuz  43006  diophun  43011  rmydioph  43252  fzunt  43692  fzuntd  43693  fzunt1d  43694  fzuntgd  43695  rp-isfinite6  43755  relexpxpmin  43954  andi3or  44261  clsk1indlem3  44280  simpcntrab  47110  zeoALTV  47912