Theorem orimdidc 812

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

Syntax hints:   -> wi 4   <-> wb 98   \/ wo 629  DECID wdc 742

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in2 545  ax-io 630

This theorem depends on definitions:  df-bi 110  df-dc 743

This theorem is referenced by:  orbididc  860