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  4232  unrab  4263  uniun  4893  unopab  5188  xpundi  5724  difxp  6167  coundir  6262  imadif  6646  unpreima  7086  soseq  8203  tpostpos  8291  elznn0nn  12734  faclbnd4lem4  14467  opsrtoslem1  22394  mbfmax  26000  fta1glem2  26517  ofmulrt  26630  lgsquadlem3  27739  nogesgn1o  28060  nosep1o  28068  noinfbnd2lem1  28117  difrab2  33166  ordtconnlem1  34626  ballotlemodife  35200  subfacp1lem6  36117  satf0op  36309  lineunray  37090  bj-axseprep  38181  wl-ifpimpr  38581  wl-df2-3mintru2  38600  poimirlem30  38760  itg2addnclem2  38782  sticksstones22  43410  lzunuz  43972  diophun  43977  rmydioph  44214  fzunt  44648  fzuntd  44649  fzunt1d  44650  fzuntgd  44651  rp-isfinite6  44711  relexpxpmin  44909  andi3or  45216  clsk1indlem3  45235  simpcntrab  48085  zeoALTV  48973  prelrrx2b  50032