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  4233  unrab  4264  uniun  4893  unopab  5189  xpundi  5728  difxp  6160  coundir  6248  imadif  6621  unpreima  7059  soseq  8161  tpostpos  8248  elznn0nn  12633  faclbnd4lem4  14364  opsrtoslem1  22277  mbfmax  25883  fta1glem2  26401  ofmulrt  26516  lgsquadlem3  27626  nogesgn1o  27917  nosep1o  27925  noinfbnd2lem1  27974  difrab2  32981  ordtconnlem1  34442  ballotlemodife  35017  subfacp1lem6  35772  satf0op  35964  lineunray  36735  bj-axseprep  37827  wl-ifpimpr  38228  wl-df2-3mintru2  38247  poimirlem30  38407  itg2addnclem2  38429  sticksstones22  43042  lzunuz  43621  diophun  43626  rmydioph  43863  fzunt  44303  fzuntd  44304  fzunt1d  44305  fzuntgd  44306  rp-isfinite6  44366  relexpxpmin  44565  andi3or  44872  clsk1indlem3  44891  simpcntrab  47706  zeoALTV  48594