Theorem orimdidc 845

Description: Disjunction distributes over implication. The forward direction, pm2.76 754, is valid intuitionistically. The reverse direction holds if ph is decidable, as can be seen at pm2.85dc 844. (Contributed by Jim Kingdon, 1-Apr-2018.)

Assertion

Ref	Expression
orimdidc	|- (DECID ph -> ( ( ph \/ ( ps -> ch ) ) <-> ( ( ph \/ ps ) -> ( ph \/ ch ) ) ) )

Proof of Theorem orimdidc

Step	Hyp	Ref	Expression
1		pm2.76 754	. 2 |- ( ( ph \/ ( ps -> ch ) ) -> ( ( ph \/ ps ) -> ( ph \/ ch ) ) )
2		pm2.85dc 844	. 2 |- (DECID ph -> ( ( ( ph \/ ps ) -> ( ph \/ ch ) ) -> ( ph \/ ( ps -> ch ) ) ) )
3	1, 2	impbid2 141	1 |- (DECID ph -> ( ( ph \/ ( ps -> ch ) ) <-> ( ( ph \/ ps ) -> ( ph \/ ch ) ) ) )

Syntax hints:   -> wi 4   <-> wb 103   \/ wo 661  DECID wdc 775

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in2 577  ax-io 662

This theorem depends on definitions:  df-bi 115  df-dc 776

This theorem is referenced by:  orbididc  894