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  4159  rabun2  4287  reuun2  4288  uniprg  4887  xpundir  5708  coundi  6220  mptun  6664  frxp2  8123  tpostpos  8225  ssfi  9137  wemapsolem  9503  ltxr  13075  hashbclem  14417  hashf1lem2  14421  pythagtriplem2  16788  pythagtrip  16805  vdwapun  16945  nosep2o  27594  legtrid  28518  colinearalg  28837  vtxdun  29409  rmoun  32423  elimifd  32472  satfvsuclem2  35347  satf0  35359  dfon2lem5  35775  seglelin  36104  bj-prmoore  37103  wl-ifp4impr  37455  wl-df4-3mintru2  37475  poimirlem30  37644  poimirlem31  37645  cnambfre  37662  fimgmcyclem  42521  expdioph  43012  dflim5  43318  rp-isfinite6  43507  uneqsn  44014