Theorem andi 1025

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∨ wo 861

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 402  df-or 862

This theorem is used by:  andir  1026  anddi  1028  cadan  1642  indi  4230  unrab  4261  uniun  4890  unopab  5185  xpundi  5720  difxp  6154  coundir  6242  imadif  6616  unpreima  7054  soseq  8160  tpostpos  8247  elznn0nn  12688  faclbnd4lem4  14420  opsrtoslem1  22344  mbfmax  25950  fta1glem2  26467  ofmulrt  26582  lgsquadlem3  27691  nogesgn1o  28012  nosep1o  28020  noinfbnd2lem1  28069  difrab2  33076  ordtconnlem1  34538  ballotlemodife  35113  subfacp1lem6  35919  satf0op  36111  lineunray  36882  bj-axseprep  37958  wl-ifpimpr  38357  wl-df2-3mintru2  38376  poimirlem30  38536  itg2addnclem2  38558  sticksstones22  43186  lzunuz  43732  diophun  43737  rmydioph  43974  fzunt  44414  fzuntd  44415  fzunt1d  44416  fzuntgd  44417  rp-isfinite6  44477  relexpxpmin  44676  andi3or  44983  clsk1indlem3  45002  simpcntrab  47824  zeoALTV  48712