Theorem andir 1026

Description: Distributive law for conjunction. (Contributed by NM, 12-Aug-1994.)

Assertion

Ref	Expression
andir	⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)))

Proof of Theorem andir

Step	Hyp	Ref	Expression
1		andi 1025	. 2 ⊢ ((𝜒 ∧ (𝜑 ∨ 𝜓)) ↔ ((𝜒 ∧ 𝜑) ∨ (𝜒 ∧ 𝜓)))
2		ancom 466	. 2 ⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜒 ∧ (𝜑 ∨ 𝜓)))
3		ancom 466	. . 3 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜒 ∧ 𝜑))
4		ancom 466	. . 3 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
5	3, 4	orbi12i 928	. 2 ⊢ (((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)) ↔ ((𝜒 ∧ 𝜑) ∨ (𝜒 ∧ 𝜓)))
6	1, 2, 5	3bitr4i 306	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:  anddi  1028  cases  1058  cador  1641  rexun  4197  rabun2  4272  reuun2  4273  uniprg  4888  xpundir  5728  coundi  6267  mptun  6715  frxp2  8198  tpostpos  8301  ssfi  9226  wemapsolem  9581  ltxr  13284  hashbclem  14638  hashf1lem2  14642  pythagtriplem2  17039  pythagtrip  17056  vdwapun  17196  nosep2o  28096  legtrid  29111  colinearalg  29545  vtxdun  30119  rmoun  33189  elimifd  33237  satfvsuclem2  36333  satf0  36345  dfon2lem5  36764  seglelin  37096  bj-prmoore  38306  wl-ifp4impr  38658  wl-df4-3mintru2  38678  poimirlem30  38836  poimirlem31  38837  cnambfre  38854  fimgmcyclem  43863  expdioph  44296  dflim5  44592  rp-isfinite6  44780  uneqsn  45286  nprmmul3  48884