Theorem andir 1008

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 1007	. 2 ⊢ ((𝜒 ∧ (𝜑 ∨ 𝜓)) ↔ ((𝜒 ∧ 𝜑) ∨ (𝜒 ∧ 𝜓)))
2		ancom 462	. 2 ⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜒 ∧ (𝜑 ∨ 𝜓)))
3		ancom 462	. . 3 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜒 ∧ 𝜑))
4		ancom 462	. . 3 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
5	3, 4	orbi12i 914	. 2 ⊢ (((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)) ↔ ((𝜒 ∧ 𝜑) ∨ (𝜒 ∧ 𝜓)))
6	1, 2, 5	3bitr4i 303	1 ⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)))

Syntax hints:   ↔ wb 205   ∧ wa 397   ∨ wo 846

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 398  df-or 847

This theorem is referenced by:  anddi  1010  cases  1042  cador  1610  rexun  4189  rabun2  4312  reuun2  4313  uniprg  4924  xpundir  5743  coundi  6243  mptun  6693  frxp2  8125  tpostpos  8226  ssfi  9169  wemapsolem  9541  ltxr  13091  hashbclem  14407  hashf1lem2  14413  pythagtriplem2  16746  pythagtrip  16763  vdwapun  16903  nosep2o  27165  legtrid  27822  colinearalg  28148  vtxdun  28718  rmoun  31712  elimifd  31753  satfvsuclem2  34289  satf0  34301  dfon2lem5  34697  seglelin  35026  bj-prmoore  35934  wl-ifp4impr  36286  wl-df4-3mintru2  36306  poimirlem30  36456  poimirlem31  36457  cnambfre  36474  expdioph  41695  dflim5  42012  rp-isfinite6  42202  uneqsn  42709