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

Theorem orimdidc 901
Description: Disjunction distributes over implication. The forward direction, pm2.76 803, is valid intuitionistically. The reverse direction holds if  ph is decidable, as can be seen at pm2.85dc 900. (Contributed by Jim Kingdon, 1-Apr-2018.)
Assertion
Ref Expression
orimdidc  |-  (DECID  ph  ->  ( ( ph  \/  ( ps  ->  ch ) )  <-> 
( ( ph  \/  ps )  ->  ( ph  \/  ch ) ) ) )

Proof of Theorem orimdidc
StepHypRef Expression
1 pm2.76 803 . 2  |-  ( (
ph  \/  ( ps  ->  ch ) )  -> 
( ( ph  \/  ps )  ->  ( ph  \/  ch ) ) )
2 pm2.85dc 900 . 2  |-  (DECID  ph  ->  ( ( ( ph  \/  ps )  ->  ( ph  \/  ch ) )  -> 
( ph  \/  ( ps  ->  ch ) ) ) )
31, 2impbid2 142 1  |-  (DECID  ph  ->  ( ( ph  \/  ( ps  ->  ch ) )  <-> 
( ( ph  \/  ps )  ->  ( ph  \/  ch ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104    \/ wo 703  DECID wdc 829
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-in2 610  ax-io 704
This theorem depends on definitions:  df-bi 116  df-dc 830
This theorem is referenced by:  orbididc  948
  Copyright terms: Public domain W3C validator