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  4146  rabun2  4274  reuun2  4275  uniprg  4875  xpundir  5686  coundi  6194  mptun  6627  frxp2  8074  tpostpos  8176  ssfi  9082  wemapsolem  9436  ltxr  13014  hashbclem  14359  hashf1lem2  14363  pythagtriplem2  16729  pythagtrip  16746  vdwapun  16886  nosep2o  27622  legtrid  28570  colinearalg  28889  vtxdun  29461  rmoun  32471  elimifd  32521  satfvsuclem2  35402  satf0  35414  dfon2lem5  35827  seglelin  36156  bj-prmoore  37155  wl-ifp4impr  37507  wl-df4-3mintru2  37527  poimirlem30  37696  poimirlem31  37697  cnambfre  37714  fimgmcyclem  42572  expdioph  43062  dflim5  43368  rp-isfinite6  43557  uneqsn  44064