Theorem andi 1023

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 972	. 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 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∨ wo 860

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 210  df-an 401  df-or 861

This theorem is referenced by:  andir  1024  anddi  1026  cadan  1632  indi  4239  unrab  4270  uniun  4891  unopab  5185  xpundi  5721  difxp  6153  coundir  6239  imadif  6609  unpreima  7048  soseq  8143  tpostpos  8230  elznn0nn  12596  faclbnd4lem4  14323  opsrtoslem1  22166  mbfmax  25769  fta1glem2  26287  ofmulrt  26401  lgsquadlem3  27504  nogesgn1o  27795  nosep1o  27803  noinfbnd2lem1  27852  difrab2  32754  ordtconnlem1  34231  ballotlemodife  34805  subfacp1lem6  35548  satf0op  35740  lineunray  36510  bj-axseprep  37571  wl-ifpimpr  37972  wl-df2-3mintru2  37991  poimirlem30  38161  itg2addnclem2  38183  sticksstones22  42797  lzunuz  43361  diophun  43366  rmydioph  43603  fzunt  44043  fzuntd  44044  fzunt1d  44045  fzuntgd  44046  rp-isfinite6  44106  relexpxpmin  44305  andi3or  44612  clsk1indlem3  44631  simpcntrab  47442  zeoALTV  48290