Theorem andi 1015

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 873	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
2		olc 874	. . 3 ⊢ ((𝜑 ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
3	1, 2	jaodan 965	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
4		orc 873	. . . 4 ⊢ (𝜓 → (𝜓 ∨ 𝜒))
5	4	anim2i 623	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
6		olc 874	. . . 4 ⊢ (𝜒 → (𝜓 ∨ 𝜒))
7	6	anim2i 623	. . 3 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
8	5, 7	jaoi 863	. 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
9	3, 8	impbii 210	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 207   ∧ wa 396   ∨ wo 853

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 208  df-an 397  df-or 854

This theorem is referenced by:  andir  1016  anddi  1018  cadan  1616  indi  4219  unrab  4250  uniun  4868  unopab  5159  xpundi  5694  difxp  6122  coundir  6206  imadif  6576  unpreima  7011  soseq  8106  tpostpos  8193  elznn0nn  12536  faclbnd4lem4  14256  opsrtoslem1  22038  mbfmax  25641  fta1glem2  26159  ofmulrt  26273  lgsquadlem3  27370  nogesgn1o  27662  nosep1o  27670  noinfbnd2lem1  27719  difrab2  32592  ordtconnlem1  34115  ballotlemodife  34689  subfacp1lem6  35420  satf0op  35612  lineunray  36382  bj-axseprep  37434  wl-ifpimpr  37835  wl-df2-3mintru2  37854  poimirlem30  38024  itg2addnclem2  38046  sticksstones22  42660  lzunuz  43224  diophun  43229  rmydioph  43466  fzunt  43906  fzuntd  43907  fzunt1d  43908  fzuntgd  43909  rp-isfinite6  43969  relexpxpmin  44168  andi3or  44475  clsk1indlem3  44494  simpcntrab  47320  zeoALTV  48168