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  4148  rabun2  4276  reuun2  4277  uniprg  4879  xpundir  5694  coundi  6205  mptun  6638  frxp2  8086  tpostpos  8188  ssfi  9097  wemapsolem  9455  ltxr  13029  hashbclem  14375  hashf1lem2  14379  pythagtriplem2  16745  pythagtrip  16762  vdwapun  16902  nosep2o  27650  legtrid  28663  colinearalg  28983  vtxdun  29555  rmoun  32568  elimifd  32618  satfvsuclem2  35554  satf0  35566  dfon2lem5  35979  seglelin  36310  bj-prmoore  37320  wl-ifp4impr  37672  wl-df4-3mintru2  37692  poimirlem30  37851  poimirlem31  37852  cnambfre  37869  fimgmcyclem  42788  expdioph  43265  dflim5  43571  rp-isfinite6  43759  uneqsn  44266