Theorem andir 1010

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∨ 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 207  df-an 396  df-or 848

This theorem is referenced by:  anddi  1012  cases  1042  cador  1609  rexun  4147  rabun2  4275  reuun2  4276  uniprg  4876  xpundir  5691  coundi  6202  mptun  6635  frxp2  8083  tpostpos  8185  ssfi  9092  wemapsolem  9446  ltxr  13024  hashbclem  14369  hashf1lem2  14373  pythagtriplem2  16739  pythagtrip  16756  vdwapun  16896  nosep2o  27631  legtrid  28579  colinearalg  28899  vtxdun  29471  rmoun  32484  elimifd  32534  satfvsuclem2  35415  satf0  35427  dfon2lem5  35840  seglelin  36171  bj-prmoore  37170  wl-ifp4impr  37522  wl-df4-3mintru2  37542  poimirlem30  37700  poimirlem31  37701  cnambfre  37718  fimgmcyclem  42641  expdioph  43130  dflim5  43436  rp-isfinite6  43625  uneqsn  44132