Theorem andir 1024

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

Syntax hints:   ↔ wb 209   ∧ wa 400   ∨ wo 860

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 210  df-an 401  df-or 861

This theorem is referenced by:  anddi  1026  cases  1056  cador  1635  rexun  4157  rabun2  4285  reuun2  4286  uniprg  4889  xpundir  5729  coundi  6245  mptun  6679  frxp2  8136  tpostpos  8238  ssfi  9153  wemapsolem  9508  ltxr  13136  hashbclem  14485  hashf1lem2  14489  pythagtriplem2  16873  pythagtrip  16890  vdwapun  17030  nosep2o  27808  legtrid  28822  colinearalg  29197  vtxdun  29768  rmoun  32777  elimifd  32826  satfvsuclem2  35747  satf0  35759  dfon2lem5  36172  seglelin  36503  bj-prmoore  37640  wl-ifp4impr  37996  wl-df4-3mintru2  38016  poimirlem30  38184  poimirlem31  38185  cnambfre  38202  fimgmcyclem  43186  expdioph  43635  dflim5  43941  rp-isfinite6  44129  uneqsn  44636  nprmmul3  48160