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  1608  rexun  4149  rabun2  4277  reuun2  4278  uniprg  4877  xpundir  5693  coundi  6200  mptun  6632  frxp2  8084  tpostpos  8186  ssfi  9097  wemapsolem  9461  ltxr  13035  hashbclem  14377  hashf1lem2  14381  pythagtriplem2  16747  pythagtrip  16764  vdwapun  16904  nosep2o  27610  legtrid  28554  colinearalg  28873  vtxdun  29445  rmoun  32456  elimifd  32505  satfvsuclem2  35335  satf0  35347  dfon2lem5  35763  seglelin  36092  bj-prmoore  37091  wl-ifp4impr  37443  wl-df4-3mintru2  37463  poimirlem30  37632  poimirlem31  37633  cnambfre  37650  fimgmcyclem  42509  expdioph  42999  dflim5  43305  rp-isfinite6  43494  uneqsn  44001