Theorem andir 1016

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 1015	. 2 ⊢ ((𝜒 ∧ (𝜑 ∨ 𝜓)) ↔ ((𝜒 ∧ 𝜑) ∨ (𝜒 ∧ 𝜓)))
2		ancom 461	. 2 ⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜒 ∧ (𝜑 ∨ 𝜓)))
3		ancom 461	. . 3 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜒 ∧ 𝜑))
4		ancom 461	. . 3 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
5	3, 4	orbi12i 920	. 2 ⊢ (((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)) ↔ ((𝜒 ∧ 𝜑) ∨ (𝜒 ∧ 𝜓)))
6	1, 2, 5	3bitr4i 304	1 ⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)))

Syntax hints:   ↔ wb 207   ∧ wa 396   ∨ wo 853

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 208  df-an 397  df-or 854

This theorem is referenced by:  anddi  1018  cases  1048  cador  1615  rexun  4125  rabun2  4252  reuun2  4253  uniprg  4854  xpundir  5688  coundi  6198  mptun  6631  frxp2  8084  tpostpos  8186  ssfi  9097  wemapsolem  9455  ltxr  13057  hashbclem  14405  hashf1lem2  14409  pythagtriplem2  16779  pythagtrip  16796  vdwapun  16936  nosep2o  27664  legtrid  28677  colinearalg  28997  vtxdun  29568  rmoun  32581  elimifd  32631  satfvsuclem2  35588  satf0  35600  dfon2lem5  36013  seglelin  36344  bj-prmoore  37473  wl-ifp4impr  37829  wl-df4-3mintru2  37849  poimirlem30  38017  poimirlem31  38018  cnambfre  38035  fimgmcyclem  43019  expdioph  43468  dflim5  43774  rp-isfinite6  43962  uneqsn  44469  nprmmul3  48004