Theorem orimdidc 906

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

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 615  ax-io 709

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

This theorem is referenced by:  orbididc  953