Theorem andi 911

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 400	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
2		olc 399	. . 3 ⊢ ((𝜑 ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
3	1, 2	jaodan 826	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
4		orc 400	. . . 4 ⊢ (𝜓 → (𝜓 ∨ 𝜒))
5	4	anim2i 593	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
6		olc 399	. . . 4 ⊢ (𝜒 → (𝜓 ∨ 𝜒))
7	6	anim2i 593	. . 3 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
8	5, 7	jaoi 394	. 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
9	3, 8	impbii 199	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 196   ∨ wo 383   ∧ wa 384

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 197  df-or 385  df-an 386

This theorem is referenced by:  andir  912  anddi  914  cadan  1548  indi  3873  indifdir  3883  unrab  3898  unipr  4449  uniun  4456  unopab  4728  xpundi  5171  difxp  5558  coundir  5637  ordnbtwnOLD  5817  imadif  5973  unpreima  6341  tpostpos  7372  elznn0nn  11391  faclbnd4lem4  13083  opsrtoslem1  19484  mbfmax  23416  fta1glem2  23926  ofmulrt  24037  lgsquadlem3  25107  difrab2  29339  ordtconnlem1  29970  ballotlemodife  30559  subfacp1lem6  31167  soseq  31751  nosep1o  31832  lineunray  32254  bj-ismooredr2  33065  poimirlem30  33439  itg2addnclem2  33462  lzunuz  37331  diophun  37337  rmydioph  37581  rp-isfinite6  37864  relexpxpmin  38009  andi3or  38320  clsk1indlem3  38341  zeoALTV  41581