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

Syntax hints:   ↔ wb 209   ∧ wa 399   ∨ 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 210  df-an 400  df-or 848

This theorem is referenced by:  anddi  1011  cases  1043  cador  1615  rexun  4104  rabun2  4228  reuun2  4229  uniprg  4836  xpundir  5618  coundi  6111  mptun  6524  tpostpos  7988  ssfi  8851  wemapsolem  9166  ltxr  12707  hashbclem  14016  hashf1lem2  14022  pythagtriplem2  16370  pythagtrip  16387  vdwapun  16527  legtrid  26682  colinearalg  27001  vtxdun  27569  rmoun  30561  elimifd  30605  satfvsuclem2  33035  satf0  33047  dfon2lem5  33482  frxp2  33528  nosep2o  33622  seglelin  34155  bj-prmoore  35021  wl-ifp4impr  35375  wl-df4-3mintru2  35395  poimirlem30  35544  poimirlem31  35545  cnambfre  35562  expdioph  40548  rp-isfinite6  40810  uneqsn  41310