ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  andi GIF version

Theorem andi 790
Description: Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)
Assertion
Ref Expression
andi ((𝜑 ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ∨ (𝜑𝜒)))

Proof of Theorem andi
StepHypRef Expression
1 orc 684 . . 3 ((𝜑𝜓) → ((𝜑𝜓) ∨ (𝜑𝜒)))
2 olc 683 . . 3 ((𝜑𝜒) → ((𝜑𝜓) ∨ (𝜑𝜒)))
31, 2jaodan 769 . 2 ((𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∨ (𝜑𝜒)))
4 orc 684 . . . 4 (𝜓 → (𝜓𝜒))
54anim2i 337 . . 3 ((𝜑𝜓) → (𝜑 ∧ (𝜓𝜒)))
6 olc 683 . . . 4 (𝜒 → (𝜓𝜒))
76anim2i 337 . . 3 ((𝜑𝜒) → (𝜑 ∧ (𝜓𝜒)))
85, 7jaoi 688 . 2 (((𝜑𝜓) ∨ (𝜑𝜒)) → (𝜑 ∧ (𝜓𝜒)))
93, 8impbii 125 1 ((𝜑 ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ∨ (𝜑𝜒)))
Colors of variables: wff set class
Syntax hints:  wa 103  wb 104  wo 680
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  andir  791  anddi  793  dcim  809  dcan  901  excxor  1339  sbequilem  1792  sborv  1844  r19.43  2564  indi  3291  difindiss  3298  unrab  3315  unipr  3718  uniun  3723  unopab  3975  xpundi  4563  coundir  5009  unpreima  5511  tpostpos  6127  elni2  7086  elznn0nn  9019
  Copyright terms: Public domain W3C validator