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  1609  rexun  4145  rabun2  4273  reuun2  4274  uniprg  4876  xpundir  5691  coundi  6201  mptun  6634  frxp2  8082  tpostpos  8184  ssfi  9091  wemapsolem  9445  ltxr  13018  hashbclem  14363  hashf1lem2  14367  pythagtriplem2  16733  pythagtrip  16750  vdwapun  16890  nosep2o  27624  legtrid  28572  colinearalg  28892  vtxdun  29464  rmoun  32477  elimifd  32527  satfvsuclem2  35427  satf0  35439  dfon2lem5  35852  seglelin  36183  bj-prmoore  37182  wl-ifp4impr  37534  wl-df4-3mintru2  37554  poimirlem30  37713  poimirlem31  37714  cnambfre  37731  fimgmcyclem  42654  expdioph  43143  dflim5  43449  rp-isfinite6  43638  uneqsn  44145