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  4149  rabun2  4277  reuun2  4278  uniprg  4890  xpundir  5733  coundi  6250  mptun  6685  frxp2  8142  tpostpos  8244  ssfi  9160  wemapsolem  9515  ltxr  13151  hashbclem  14502  hashf1lem2  14506  pythagtriplem2  16894  pythagtrip  16911  vdwapun  17051  nosep2o  27875  legtrid  28889  colinearalg  29289  vtxdun  29860  rmoun  32869  elimifd  32918  satfvsuclem2  35865  satf0  35877  dfon2lem5  36290  seglelin  36621  bj-prmoore  37790  wl-ifp4impr  38146  wl-df4-3mintru2  38166  poimirlem30  38334  poimirlem31  38335  cnambfre  38352  fimgmcyclem  43334  expdioph  43783  dflim5  44089  rp-isfinite6  44277  uneqsn  44784  nprmmul3  48311