Theorem orim2d 885

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 24	. 2 |- ( ph -> ( th -> th ) )
2		orim1d.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	orim12d 883	1 |- ( ph -> ( ( th \/ ps ) -> ( th \/ ch ) ) )

Syntax hints:   -> wi 4   \/ wo 383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386

This theorem is referenced by:  orim2  886  pm2.82  897  poxp  7289  soxp  7290  relin01  10552  nneo  11461  uzp1  11721  vdwlem9  15693  dfconn2  21222  fin1aufil  21736  dgrlt  24022  aalioulem2  24088  aalioulem5  24091  aalioulem6  24092  aaliou  24093  sqff1o  24908  disjpreima  29397  disjdsct  29480  voliune  30292  volfiniune  30293  naim2  32385  paddss2  35104  lzunuz  37331  acongneg2  37544  nneom  42321