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  1610  rexun  4136  rabun2  4264  reuun2  4265  uniprg  4866  xpundir  5701  coundi  6211  mptun  6644  frxp2  8094  tpostpos  8196  ssfi  9107  wemapsolem  9465  ltxr  13066  hashbclem  14414  hashf1lem2  14418  pythagtriplem2  16788  pythagtrip  16805  vdwapun  16945  nosep2o  27646  legtrid  28659  colinearalg  28979  vtxdun  29550  rmoun  32563  elimifd  32613  satfvsuclem2  35542  satf0  35554  dfon2lem5  35967  seglelin  36298  bj-prmoore  37427  wl-ifp4impr  37783  wl-df4-3mintru2  37803  poimirlem30  37971  poimirlem31  37972  cnambfre  37989  fimgmcyclem  42978  expdioph  43451  dflim5  43757  rp-isfinite6  43945  uneqsn  44452  nprmmul3  47989