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

Theorem andi 807
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  |-  ( (
ph  /\  ( ps  \/  ch ) )  <->  ( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )

Proof of Theorem andi
StepHypRef Expression
1 orc 701 . . 3  |-  ( (
ph  /\  ps )  ->  ( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
2 olc 700 . . 3  |-  ( (
ph  /\  ch )  ->  ( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
31, 2jaodan 786 . 2  |-  ( (
ph  /\  ( ps  \/  ch ) )  -> 
( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
4 orc 701 . . . 4  |-  ( ps 
->  ( ps  \/  ch ) )
54anim2i 339 . . 3  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ( ps  \/  ch ) ) )
6 olc 700 . . . 4  |-  ( ch 
->  ( ps  \/  ch ) )
76anim2i 339 . . 3  |-  ( (
ph  /\  ch )  ->  ( ph  /\  ( ps  \/  ch ) ) )
85, 7jaoi 705 . 2  |-  ( ( ( ph  /\  ps )  \/  ( ph  /\ 
ch ) )  -> 
( ph  /\  ( ps  \/  ch ) ) )
93, 8impbii 125 1  |-  ( (
ph  /\  ( ps  \/  ch ) )  <->  ( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 103    <-> wb 104    \/ wo 697
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 698
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  andir  808  anddi  810  dcim  826  dcan  918  excxor  1356  sbequilem  1810  sborv  1862  r19.43  2587  indi  3318  difindiss  3325  unrab  3342  unipr  3745  uniun  3750  unopab  4002  xpundi  4590  coundir  5036  unpreima  5538  tpostpos  6154  elni2  7115  elznn0nn  9061
  Copyright terms: Public domain W3C validator