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  5721  coundi  6247  mptun  6683  frxp2  8154  tpostpos  8256  ssfi  9181  wemapsolem  9537  ltxr  13237  hashbclem  14590  hashf1lem2  14594  pythagtriplem2  16988  pythagtrip  17005  vdwapun  17145  nosep2o  28032  legtrid  29047  colinearalg  29481  vtxdun  30055  rmoun  33083  elimifd  33132  satfvsuclem2  36104  satf0  36116  dfon2lem5  36529  seglelin  36861  bj-prmoore  38016  wl-ifp4impr  38370  wl-df4-3mintru2  38390  poimirlem30  38548  poimirlem31  38549  cnambfre  38566  fimgmcyclem  43577  expdioph  44009  dflim5  44315  rp-isfinite6  44503  uneqsn  45010  nprmmul3  48580