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  4150  rabun2  4278  reuun2  4279  uniprg  4881  xpundir  5702  coundi  6213  mptun  6646  frxp2  8096  tpostpos  8198  ssfi  9109  wemapsolem  9467  ltxr  13041  hashbclem  14387  hashf1lem2  14391  pythagtriplem2  16757  pythagtrip  16774  vdwapun  16914  nosep2o  27662  legtrid  28675  colinearalg  28995  vtxdun  29567  rmoun  32579  elimifd  32629  satfvsuclem2  35573  satf0  35585  dfon2lem5  35998  seglelin  36329  bj-prmoore  37365  wl-ifp4impr  37719  wl-df4-3mintru2  37739  poimirlem30  37898  poimirlem31  37899  cnambfre  37916  fimgmcyclem  42900  expdioph  43377  dflim5  43683  rp-isfinite6  43871  uneqsn  44378