Theorem andir 1021

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 1020	. 2 ⊢ ((𝜒 ∧ (𝜑 ∨ 𝜓)) ↔ ((𝜒 ∧ 𝜑) ∨ (𝜒 ∧ 𝜓)))
2		ancom 464	. 2 ⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜒 ∧ (𝜑 ∨ 𝜓)))
3		ancom 464	. . 3 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜒 ∧ 𝜑))
4		ancom 464	. . 3 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
5	3, 4	orbi12i 925	. 2 ⊢ (((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)) ↔ ((𝜒 ∧ 𝜑) ∨ (𝜒 ∧ 𝜓)))
6	1, 2, 5	3bitr4i 305	1 ⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)))

Syntax hints:   ↔ wb 208   ∧ wa 399   ∨ wo 858

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 209  df-an 400  df-or 859

This theorem is referenced by:  anddi  1023  cases  1053  cador  1627  rexun  4146  rabun2  4274  reuun2  4275  uniprg  4878  xpundir  5713  coundi  6229  mptun  6662  frxp2  8118  tpostpos  8220  ssfi  9135  wemapsolem  9492  ltxr  13111  hashbclem  14459  hashf1lem2  14463  pythagtriplem2  16844  pythagtrip  16861  vdwapun  17001  nosep2o  27734  legtrid  28748  colinearalg  29068  vtxdun  29639  rmoun  32652  elimifd  32702  satfvsuclem2  35671  satf0  35683  dfon2lem5  36096  seglelin  36427  bj-prmoore  37566  wl-ifp4impr  37922  wl-df4-3mintru2  37942  poimirlem30  38110  poimirlem31  38111  cnambfre  38128  fimgmcyclem  43112  expdioph  43561  dflim5  43867  rp-isfinite6  44055  uneqsn  44562  nprmmul3  48096