Theorem andir 1026

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 1025	. 2 ⊢ ((𝜒 ∧ (𝜑 ∨ 𝜓)) ↔ ((𝜒 ∧ 𝜑) ∨ (𝜒 ∧ 𝜓)))
2		ancom 465	. 2 ⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜒 ∧ (𝜑 ∨ 𝜓)))
3		ancom 465	. . 3 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜒 ∧ 𝜑))
4		ancom 465	. . 3 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
5	3, 4	orbi12i 927	. 2 ⊢ (((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)) ↔ ((𝜒 ∧ 𝜑) ∨ (𝜒 ∧ 𝜓)))
6	1, 2, 5	3bitr4i 306	1 ⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∨ wo 860

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 210  df-an 401  df-or 861

This theorem is referenced by:  anddi  1028  cases  1058  cador  1638  rexun  4150  rabun2  4278  reuun2  4279  uniprg  4889  xpundir  5733  coundi  6250  mptun  6683  frxp2  8141  tpostpos  8243  ssfi  9158  wemapsolem  9513  ltxr  13141  hashbclem  14491  hashf1lem2  14495  pythagtriplem2  16878  pythagtrip  16895  vdwapun  17035  nosep2o  27827  legtrid  28841  colinearalg  29241  vtxdun  29812  rmoun  32821  elimifd  32870  satfvsuclem2  35833  satf0  35845  dfon2lem5  36258  seglelin  36589  bj-prmoore  37738  wl-ifp4impr  38094  wl-df4-3mintru2  38114  poimirlem30  38282  poimirlem31  38283  cnambfre  38300  fimgmcyclem  43284  expdioph  43733  dflim5  44039  rp-isfinite6  44227  uneqsn  44734  nprmmul3  48261