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

Syntax hints:   ↔ wb 205   ∧ wa 396   ∨ wo 844

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 397  df-or 845

This theorem is referenced by:  anddi  1008  cases  1040  cador  1610  rexun  4124  rabun2  4247  reuun2  4248  uniprg  4856  xpundir  5656  coundi  6151  mptun  6579  tpostpos  8062  ssfi  8956  wemapsolem  9309  ltxr  12851  hashbclem  14164  hashf1lem2  14170  pythagtriplem2  16518  pythagtrip  16535  vdwapun  16675  legtrid  26952  colinearalg  27278  vtxdun  27848  rmoun  30842  elimifd  30886  satfvsuclem2  33322  satf0  33334  dfon2lem5  33763  frxp2  33791  nosep2o  33885  seglelin  34418  bj-prmoore  35286  wl-ifp4impr  35638  wl-df4-3mintru2  35658  poimirlem30  35807  poimirlem31  35808  cnambfre  35825  expdioph  40845  rp-isfinite6  41125  uneqsn  41633