Theorem orim2d 800

Description: Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)

Hypothesis

Ref	Expression
orim1d.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
orim2d	|- ( ph -> ( ( th \/ ps ) -> ( th \/ ch ) ) )

Proof of Theorem orim2d

Step	Hyp	Ref	Expression
1		idd 21	. 2 |- ( ph -> ( th -> th ) )
2		orim1d.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	orim12d 798	1 |- ( ph -> ( ( th \/ ps ) -> ( th \/ ch ) ) )

Syntax hints:   -> wi 4   \/ wo 720

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-io 721

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim2  801  orbi2d  802  pm2.82  824  stdcndcOLD  858  pm2.13dc  897  exmid1dc  4332  acexmidlemcase  6070  poxp  6458  fodjuomnilemdc  7474  omniwomnimkv  7497  exmidontriimlem1  7567  indpi  7699  suplocexprlemloc  8078  nneoor  9727  uzp1  9935  maxabslemlub  11951  xrmaxiflemlub  11992  nninfctlemfo  12795  exmidunben  13295  bj-nn0suc  16904  sbthomlem  16975