Theorem orimdidc 907

Description: Disjunction distributes over implication. The forward direction, pm2.76 809, is valid intuitionistically. The reverse direction holds if ph is decidable, as can be seen at pm2.85dc 906. (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 809	. 2 |- ( ( ph \/ ( ps -> ch ) ) -> ( ( ph \/ ps ) -> ( ph \/ ch ) ) )
2		pm2.85dc 906	. 2 |- (DECID ph -> ( ( ( ph \/ ps ) -> ( ph \/ ch ) ) -> ( ph \/ ( ps -> ch ) ) ) )
3	1, 2	impbid2 143	1 |- (DECID ph -> ( ( ph \/ ( ps -> ch ) ) <-> ( ( ph \/ ps ) -> ( ph \/ ch ) ) ) )

Syntax hints:   -> wi 4   <-> wb 105   \/ wo 709  DECID wdc 835

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 616  ax-io 710

This theorem depends on definitions:  df-bi 117  df-dc 836

This theorem is referenced by:  orbididc  955