Theorem orim2d 778

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 776	1 |- ( ph -> ( ( th \/ ps ) -> ( th \/ ch ) ) )

Syntax hints:   -> wi 4   \/ wo 698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orim2  779  orbi2d  780  pm2.82  802  stdcndcOLD  832  pm2.13dc  871  exmid1dc  4161  acexmidlemcase  5816  poxp  6176  fodjuomnilemdc  7081  omniwomnimkv  7104  exmidontriimlem1  7150  indpi  7256  suplocexprlemloc  7635  nneoor  9260  uzp1  9466  maxabslemlub  11100  xrmaxiflemlub  11138  exmidunben  12138  bj-nn0suc  13510  sbthomlem  13567