Theorem andir 1010

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 1009	. 2 ⊢ ((𝜒 ∧ (𝜑 ∨ 𝜓)) ↔ ((𝜒 ∧ 𝜑) ∨ (𝜒 ∧ 𝜓)))
2		ancom 460	. 2 ⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜒 ∧ (𝜑 ∨ 𝜓)))
3		ancom 460	. . 3 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜒 ∧ 𝜑))
4		ancom 460	. . 3 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
5	3, 4	orbi12i 914	. 2 ⊢ (((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)) ↔ ((𝜒 ∧ 𝜑) ∨ (𝜒 ∧ 𝜓)))
6	1, 2, 5	3bitr4i 303	1 ⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∨ wo 847

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 207  df-an 396  df-or 848

This theorem is referenced by:  anddi  1012  cases  1042  cador  1605  rexun  4206  rabun2  4330  reuun2  4331  uniprg  4928  xpundir  5758  coundi  6269  mptun  6715  frxp2  8168  tpostpos  8270  ssfi  9212  wemapsolem  9588  ltxr  13155  hashbclem  14488  hashf1lem2  14492  pythagtriplem2  16851  pythagtrip  16868  vdwapun  17008  nosep2o  27742  legtrid  28614  colinearalg  28940  vtxdun  29514  rmoun  32522  elimifd  32564  satfvsuclem2  35345  satf0  35357  dfon2lem5  35769  seglelin  36098  bj-prmoore  37098  wl-ifp4impr  37450  wl-df4-3mintru2  37470  poimirlem30  37637  poimirlem31  37638  cnambfre  37655  fimgmcyclem  42520  expdioph  43012  dflim5  43319  rp-isfinite6  43508  uneqsn  44015