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  1606  indi  4290  unrab  4321  uniun  4935  unopab  5230  xpundi  5757  difxp  6186  coundir  6270  imadif  6652  unpreima  7083  soseq  8183  tpostpos  8270  elznn0nn  12625  faclbnd4lem4  14332  opsrtoslem1  22097  mbfmax  25698  fta1glem2  26223  ofmulrt  26338  lgsquadlem3  27441  nogesgn1o  27733  nosep1o  27741  noinfbnd2lem1  27790  difrab2  32526  ordtconnlem1  33885  ballotlemodife  34479  subfacp1lem6  35170  satf0op  35362  lineunray  36129  wl-ifpimpr  37449  wl-df2-3mintru2  37468  poimirlem30  37637  itg2addnclem2  37659  sticksstones22  42150  lzunuz  42756  diophun  42761  rmydioph  43003  fzunt  43445  fzuntd  43446  fzunt1d  43447  fzuntgd  43448  rp-isfinite6  43508  relexpxpmin  43707  andi3or  44014  clsk1indlem3  44033  simpcntrab  46826  zeoALTV  47595