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  836  pm2.13dc  875  exmid1dc  4179  acexmidlemcase  5837  poxp  6200  fodjuomnilemdc  7108  omniwomnimkv  7131  exmidontriimlem1  7177  indpi  7283  suplocexprlemloc  7662  nneoor  9293  uzp1  9499  maxabslemlub  11149  xrmaxiflemlub  11189  exmidunben  12359  bj-nn0suc  13846  sbthomlem  13904