Theorem andir 1026

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by:  anddi  1028  cases  1058  cador  1641  rexun  4142  rabun2  4270  reuun2  4271  uniprg  4883  xpundir  5725  coundi  6243  mptun  6678  frxp2  8142  tpostpos  8244  ssfi  9167  wemapsolem  9522  ltxr  13166  hashbclem  14517  hashf1lem2  14521  pythagtriplem2  16909  pythagtrip  16926  vdwapun  17066  nosep2o  27918  legtrid  28933  colinearalg  29367  vtxdun  29941  rmoun  32969  elimifd  33018  satfvsuclem2  35939  satf0  35951  dfon2lem5  36364  seglelin  36696  bj-prmoore  37865  wl-ifp4impr  38221  wl-df4-3mintru2  38241  poimirlem30  38399  poimirlem31  38400  cnambfre  38417  fimgmcyclem  43415  expdioph  43864  dflim5  44170  rp-isfinite6  44358  uneqsn  44865  nprmmul3  48429