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

Theorem orimdidc 874
Description: Disjunction distributes over implication. The forward direction, pm2.76 780, is valid intuitionistically. The reverse direction holds if  ph is decidable, as can be seen at pm2.85dc 873. (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 780 . 2  |-  ( (
ph  \/  ( ps  ->  ch ) )  -> 
( ( ph  \/  ps )  ->  ( ph  \/  ch ) ) )
2 pm2.85dc 873 . 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 680  DECID wdc 802
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 587  ax-io 681
This theorem depends on definitions:  df-bi 116  df-dc 803
This theorem is referenced by:  orbididc  920
  Copyright terms: Public domain W3C validator