Theorem andir 1006

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 1005	. 2 ⊢ ((𝜒 ∧ (𝜑 ∨ 𝜓)) ↔ ((𝜒 ∧ 𝜑) ∨ (𝜒 ∧ 𝜓)))
2		ancom 459	. 2 ⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜒 ∧ (𝜑 ∨ 𝜓)))
3		ancom 459	. . 3 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜒 ∧ 𝜑))
4		ancom 459	. . 3 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
5	3, 4	orbi12i 912	. 2 ⊢ (((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)) ↔ ((𝜒 ∧ 𝜑) ∨ (𝜒 ∧ 𝜓)))
6	1, 2, 5	3bitr4i 302	1 ⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)))

Syntax hints:   ↔ wb 205   ∧ wa 394   ∨ wo 845

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 206  df-an 395  df-or 846

This theorem is referenced by:  anddi  1008  cases  1040  cador  1602  rexun  4201  rabun2  4326  reuun2  4327  uniprg  4934  xpundir  5755  coundi  6263  mptun  6711  frxp2  8166  tpostpos  8269  ssfi  9219  wemapsolem  9600  ltxr  13159  hashbclem  14481  hashf1lem2  14487  pythagtriplem2  16840  pythagtrip  16857  vdwapun  16997  nosep2o  27735  legtrid  28541  colinearalg  28867  vtxdun  29441  rmoun  32445  elimifd  32490  satfvsuclem2  35235  satf0  35247  dfon2lem5  35658  seglelin  35987  bj-prmoore  36869  wl-ifp4impr  37221  wl-df4-3mintru2  37241  poimirlem30  37398  poimirlem31  37399  cnambfre  37416  fimgmcyclem  42257  expdioph  42752  dflim5  43066  rp-isfinite6  43256  uneqsn  43763