Theorem andir 1008

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

Syntax hints:   ↔ wb 205   ∧ wa 397   ∨ wo 846

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 206  df-an 398  df-or 847

This theorem is referenced by:  anddi  1010  cases  1042  cador  1610  rexun  4191  rabun2  4314  reuun2  4315  uniprg  4926  xpundir  5746  coundi  6247  mptun  6697  frxp2  8130  tpostpos  8231  ssfi  9173  wemapsolem  9545  ltxr  13095  hashbclem  14411  hashf1lem2  14417  pythagtriplem2  16750  pythagtrip  16767  vdwapun  16907  nosep2o  27185  legtrid  27842  colinearalg  28168  vtxdun  28738  rmoun  31734  elimifd  31775  satfvsuclem2  34351  satf0  34363  dfon2lem5  34759  seglelin  35088  bj-prmoore  35996  wl-ifp4impr  36348  wl-df4-3mintru2  36368  poimirlem30  36518  poimirlem31  36519  cnambfre  36536  expdioph  41762  dflim5  42079  rp-isfinite6  42269  uneqsn  42776