Theorem andi 947

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 399	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
2		olc 398	. . 3 ⊢ ((𝜑 ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
3	1, 2	jaodan 861	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
4		orc 399	. . . 4 ⊢ (𝜓 → (𝜓 ∨ 𝜒))
5	4	anim2i 594	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
6		olc 398	. . . 4 ⊢ (𝜒 → (𝜓 ∨ 𝜒))
7	6	anim2i 594	. . 3 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
8	5, 7	jaoi 393	. 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
9	3, 8	impbii 199	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 196   ∨ wo 382   ∧ wa 383

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 197  df-or 384  df-an 385

This theorem is referenced by:  andir  948  anddi  950  annotanannotOLD  978  cadan  1697  indi  4016  indifdir  4026  unrab  4041  unipr  4601  uniun  4608  unopab  4880  xpundi  5328  difxp  5716  coundir  5798  ordnbtwnOLD  5978  imadif  6134  unpreima  6504  tpostpos  7541  elznn0nn  11583  faclbnd4lem4  13277  opsrtoslem1  19686  mbfmax  23615  fta1glem2  24125  ofmulrt  24236  lgsquadlem3  25306  difrab2  29646  ordtconnlem1  30279  ballotlemodife  30868  subfacp1lem6  31474  soseq  32060  nosep1o  32138  lineunray  32560  bj-ismooredr2  33371  poimirlem30  33752  itg2addnclem2  33775  lzunuz  37833  diophun  37839  rmydioph  38083  rp-isfinite6  38366  relexpxpmin  38511  andi3or  38822  clsk1indlem3  38843  zeoALTV  42091