Theorem andir 1005

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 1004	. 2 ⊢ ((𝜒 ∧ (𝜑 ∨ 𝜓)) ↔ ((𝜒 ∧ 𝜑) ∨ (𝜒 ∧ 𝜓)))
2		ancom 460	. 2 ⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜒 ∧ (𝜑 ∨ 𝜓)))
3		ancom 460	. . 3 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜒 ∧ 𝜑))
4		ancom 460	. . 3 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
5	3, 4	orbi12i 911	. 2 ⊢ (((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)) ↔ ((𝜒 ∧ 𝜑) ∨ (𝜒 ∧ 𝜓)))
6	1, 2, 5	3bitr4i 302	1 ⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)))

Syntax hints:   ↔ wb 205   ∧ wa 395   ∨ wo 843

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 206  df-an 396  df-or 844

This theorem is referenced by:  anddi  1007  cases  1039  cador  1611  rexun  4120  rabun2  4244  reuun2  4245  uniprg  4853  xpundir  5647  coundi  6140  mptun  6563  tpostpos  8033  ssfi  8918  wemapsolem  9239  ltxr  12780  hashbclem  14092  hashf1lem2  14098  pythagtriplem2  16446  pythagtrip  16463  vdwapun  16603  legtrid  26856  colinearalg  27181  vtxdun  27751  rmoun  30743  elimifd  30787  satfvsuclem2  33222  satf0  33234  dfon2lem5  33669  frxp2  33718  nosep2o  33812  seglelin  34345  bj-prmoore  35213  wl-ifp4impr  35565  wl-df4-3mintru2  35585  poimirlem30  35734  poimirlem31  35735  cnambfre  35752  expdioph  40761  rp-isfinite6  41023  uneqsn  41522