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

Step	Hyp	Ref	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 ) ) ) )
3	1, 2	impbid2 142	1 |- (DECID ph -> ( ( ph \/ ( ps -> ch ) ) <-> ( ( ph \/ ps ) -> ( ph \/ ch ) ) ) )

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