Theorem andi 1035

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 898	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
2		olc 899	. . 3 ⊢ ((𝜑 ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
3	1, 2	jaodan 985	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
4		orc 898	. . . 4 ⊢ (𝜓 → (𝜓 ∨ 𝜒))
5	4	anim2i 610	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
6		olc 899	. . . 4 ⊢ (𝜒 → (𝜓 ∨ 𝜒))
7	6	anim2i 610	. . 3 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
8	5, 7	jaoi 888	. 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
9	3, 8	impbii 201	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 198   ∧ wa 386   ∨ wo 878

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 199  df-an 387  df-or 879

This theorem is referenced by:  andir  1036  anddi  1038  annotanannotOLD  1039  cadan  1722  indi  4103  indifdir  4113  unrab  4127  unipr  4671  uniun  4679  unopab  4951  xpundi  5404  difxp  5799  coundir  5878  imadif  6206  unpreima  6590  tpostpos  7637  elznn0nn  11718  faclbnd4lem4  13376  opsrtoslem1  19844  mbfmax  23815  fta1glem2  24325  ofmulrt  24436  lgsquadlem3  25520  difrab2  29876  ordtconnlem1  30504  ballotlemodife  31094  subfacp1lem6  31702  soseq  32282  nosep1o  32360  lineunray  32782  bj-ismooredr2  33581  poimirlem30  33976  itg2addnclem2  33998  lzunuz  38168  diophun  38174  rmydioph  38417  rp-isfinite6  38698  relexpxpmin  38843  andi3or  39153  clsk1indlem3  39174  zeoALTV  42404