Theorem andir 1010

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∨ wo 847

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 207  df-an 396  df-or 848

This theorem is referenced by:  anddi  1012  cases  1042  cador  1608  rexun  4162  rabun2  4290  reuun2  4291  uniprg  4890  xpundir  5711  coundi  6223  mptun  6667  frxp2  8126  tpostpos  8228  ssfi  9143  wemapsolem  9510  ltxr  13082  hashbclem  14424  hashf1lem2  14428  pythagtriplem2  16795  pythagtrip  16812  vdwapun  16952  nosep2o  27601  legtrid  28525  colinearalg  28844  vtxdun  29416  rmoun  32430  elimifd  32479  satfvsuclem2  35354  satf0  35366  dfon2lem5  35782  seglelin  36111  bj-prmoore  37110  wl-ifp4impr  37462  wl-df4-3mintru2  37482  poimirlem30  37651  poimirlem31  37652  cnambfre  37669  fimgmcyclem  42528  expdioph  43019  dflim5  43325  rp-isfinite6  43514  uneqsn  44021