Theorem andir 1011

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

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

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 849

This theorem is referenced by:  anddi  1013  cases  1043  cador  1608  rexun  4196  rabun2  4324  reuun2  4325  uniprg  4923  xpundir  5755  coundi  6267  mptun  6714  frxp2  8169  tpostpos  8271  ssfi  9213  wemapsolem  9590  ltxr  13157  hashbclem  14491  hashf1lem2  14495  pythagtriplem2  16855  pythagtrip  16872  vdwapun  17012  nosep2o  27727  legtrid  28599  colinearalg  28925  vtxdun  29499  rmoun  32513  elimifd  32556  satfvsuclem2  35365  satf0  35377  dfon2lem5  35788  seglelin  36117  bj-prmoore  37116  wl-ifp4impr  37468  wl-df4-3mintru2  37488  poimirlem30  37657  poimirlem31  37658  cnambfre  37675  fimgmcyclem  42543  expdioph  43035  dflim5  43342  rp-isfinite6  43531  uneqsn  44038