Theorem andir 1011

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

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

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 849

This theorem is referenced by:  anddi  1013  cases  1043  cador  1610  rexun  4137  rabun2  4265  reuun2  4266  uniprg  4867  xpundir  5694  coundi  6205  mptun  6638  frxp2  8087  tpostpos  8189  ssfi  9100  wemapsolem  9458  ltxr  13057  hashbclem  14405  hashf1lem2  14409  pythagtriplem2  16779  pythagtrip  16796  vdwapun  16936  nosep2o  27660  legtrid  28673  colinearalg  28993  vtxdun  29565  rmoun  32578  elimifd  32628  satfvsuclem2  35558  satf0  35570  dfon2lem5  35983  seglelin  36314  bj-prmoore  37443  wl-ifp4impr  37797  wl-df4-3mintru2  37817  poimirlem30  37985  poimirlem31  37986  cnambfre  38003  fimgmcyclem  42992  expdioph  43469  dflim5  43775  rp-isfinite6  43963  uneqsn  44470  nprmmul3  48001