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  1640  rexun  4194  rabun2  4269  reuun2  4270  uniprg  4882  xpundir  5720  coundi  6248  mptun  6686  frxp2  8164  tpostpos  8267  ssfi  9192  wemapsolem  9548  ltxr  13248  hashbclem  14601  hashf1lem2  14605  pythagtriplem2  17001  pythagtrip  17018  vdwapun  17158  nosep2o  28045  legtrid  29060  colinearalg  29494  vtxdun  30068  rmoun  33138  elimifd  33187  satfvsuclem2  36212  satf0  36224  dfon2lem5  36642  seglelin  36974  bj-prmoore  38129  wl-ifp4impr  38484  wl-df4-3mintru2  38504  poimirlem30  38662  poimirlem31  38663  cnambfre  38680  fimgmcyclem  43691  expdioph  44124  dflim5  44425  rp-isfinite6  44613  uneqsn  45119  nprmmul3  48705