Theorem andi 1010

Description: Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)

Assertion

Ref	Expression
andi	⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))

Proof of Theorem andi

Step	Hyp	Ref	Expression
1		orc 868	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
2		olc 869	. . 3 ⊢ ((𝜑 ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
3	1, 2	jaodan 960	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
4		orc 868	. . . 4 ⊢ (𝜓 → (𝜓 ∨ 𝜒))
5	4	anim2i 618	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
6		olc 869	. . . 4 ⊢ (𝜒 → (𝜓 ∨ 𝜒))
7	6	anim2i 618	. . 3 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
8	5, 7	jaoi 858	. 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
9	3, 8	impbii 209	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:  andir  1011  anddi  1013  cadan  1611  indi  4225  unrab  4256  uniun  4874  unopab  5166  xpundi  5693  difxp  6122  coundir  6206  imadif  6576  unpreima  7009  soseq  8102  tpostpos  8189  elznn0nn  12529  faclbnd4lem4  14249  opsrtoslem1  22043  mbfmax  25626  fta1glem2  26144  ofmulrt  26258  lgsquadlem3  27359  nogesgn1o  27651  nosep1o  27659  noinfbnd2lem1  27708  difrab2  32582  ordtconnlem1  34084  ballotlemodife  34658  subfacp1lem6  35383  satf0op  35575  lineunray  36345  bj-axseprep  37397  wl-ifpimpr  37796  wl-df2-3mintru2  37815  poimirlem30  37985  itg2addnclem2  38007  sticksstones22  42621  lzunuz  43214  diophun  43219  rmydioph  43460  fzunt  43900  fzuntd  43901  fzunt1d  43902  fzuntgd  43903  rp-isfinite6  43963  relexpxpmin  44162  andi3or  44469  clsk1indlem3  44488  simpcntrab  47316  zeoALTV  48158