Theorem orim2d 783

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

Syntax hints:   -> wi 4   \/ wo 703

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 704

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orim2  784  orbi2d  785  pm2.82  807  stdcndcOLD  841  pm2.13dc  880  exmid1dc  4186  acexmidlemcase  5848  poxp  6211  fodjuomnilemdc  7120  omniwomnimkv  7143  exmidontriimlem1  7198  indpi  7304  suplocexprlemloc  7683  nneoor  9314  uzp1  9520  maxabslemlub  11171  xrmaxiflemlub  11211  exmidunben  12381  bj-nn0suc  13999  sbthomlem  14057