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  4171  rabun2  4299  reuun2  4300  uniprg  4899  xpundir  5724  coundi  6236  mptun  6684  frxp2  8143  tpostpos  8245  ssfi  9187  wemapsolem  9564  ltxr  13131  hashbclem  14470  hashf1lem2  14474  pythagtriplem2  16837  pythagtrip  16854  vdwapun  16994  nosep2o  27646  legtrid  28570  colinearalg  28889  vtxdun  29461  rmoun  32475  elimifd  32524  satfvsuclem2  35382  satf0  35394  dfon2lem5  35805  seglelin  36134  bj-prmoore  37133  wl-ifp4impr  37485  wl-df4-3mintru2  37505  poimirlem30  37674  poimirlem31  37675  cnambfre  37692  fimgmcyclem  42556  expdioph  43047  dflim5  43353  rp-isfinite6  43542  uneqsn  44049