Theorem andir 1009

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

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

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 847

This theorem is referenced by:  anddi  1011  cases  1043  cador  1605  rexun  4219  rabun2  4343  reuun2  4344  uniprg  4947  xpundir  5769  coundi  6278  mptun  6726  frxp2  8185  tpostpos  8287  ssfi  9240  wemapsolem  9619  ltxr  13178  hashbclem  14501  hashf1lem2  14505  pythagtriplem2  16864  pythagtrip  16881  vdwapun  17021  nosep2o  27745  legtrid  28617  colinearalg  28943  vtxdun  29517  rmoun  32522  elimifd  32566  satfvsuclem2  35328  satf0  35340  dfon2lem5  35751  seglelin  36080  bj-prmoore  37081  wl-ifp4impr  37433  wl-df4-3mintru2  37453  poimirlem30  37610  poimirlem31  37611  cnambfre  37628  fimgmcyclem  42488  expdioph  42980  dflim5  43291  rp-isfinite6  43480  uneqsn  43987