Theorem andi 1024

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 880	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
2		olc 881	. . 3 ⊢ ((𝜑 ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
3	1, 2	jaodan 971	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
4		orc 880	. . . 4 ⊢ (𝜓 → (𝜓 ∨ 𝜒))
5	4	anim2i 628	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
6		olc 881	. . . 4 ⊢ (𝜒 → (𝜓 ∨ 𝜒))
7	6	anim2i 628	. . 3 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
8	5, 7	jaoi 870	. 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
9	3, 8	impbii 212	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 400   ∨ wo 860

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861

This theorem is used by:  andir  1025  anddi  1027  cadan  1638  indi  4236  unrab  4267  uniun  4894  unopab  5190  xpundi  5729  difxp  6160  coundir  6248  imadif  6620  unpreima  7058  soseq  8153  tpostpos  8240  elznn0nn  12611  faclbnd4lem4  14339  opsrtoslem1  22217  mbfmax  25819  fta1glem2  26337  ofmulrt  26451  lgsquadlem3  27557  nogesgn1o  27848  nosep1o  27856  noinfbnd2lem1  27905  difrab2  32855  ordtconnlem1  34323  ballotlemodife  34897  subfacp1lem6  35685  satf0op  35877  lineunray  36647  bj-axseprep  37739  wl-ifpimpr  38140  wl-df2-3mintru2  38159  poimirlem30  38329  itg2addnclem2  38351  sticksstones22  42963  lzunuz  43527  diophun  43532  rmydioph  43769  fzunt  44209  fzuntd  44210  fzunt1d  44211  fzuntgd  44212  rp-isfinite6  44272  relexpxpmin  44471  andi3or  44778  clsk1indlem3  44797  simpcntrab  47612  zeoALTV  48463