Theorem orim12d 732

Description: Disjoin antecedents and consequents in a deduction. (Contributed by NM, 10-May-1994.)

Hypotheses

Ref	Expression
orim12d.1	|- ( ph -> ( ps -> ch ) )
orim12d.2	|- ( ph -> ( th -> ta ) )

Assertion

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

Proof of Theorem orim12d

Step	Hyp	Ref	Expression
1		orim12d.1	. 2 |- ( ph -> ( ps -> ch ) )
2		orim12d.2	. 2 |- ( ph -> ( th -> ta ) )
3		pm3.48 731	. 2 |- ( ( ( ps -> ch ) /\ ( th -> ta ) ) -> ( ( ps \/ th ) -> ( ch \/ ta ) ) )
4	1, 2, 3	syl2anc 403	1 |- ( ph -> ( ( ps \/ th ) -> ( ch \/ ta ) ) )

Syntax hints:   -> wi 4   \/ wo 661

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  orim1d  733  orim2d  734  3orim123d  1251  19.33b2  1560  preq12b  3562  prel12  3563  funun  4964  nnsucelsuc  6093  nnaord  6105  nnmord  6113  swoer  6157  fidceq  6354  fin0or  6370  ltsopr  6786  cauappcvgprlemloc  6842  caucvgprlemloc  6865  caucvgprprlemloc  6893  mulextsr1lem  6956  reapcotr  7698  apcotr  7707  mulext1  7712  mulext  7714  peano2z  8387  zeo  8452  uzm1  8649  eluzdc  8697  fzospliti  9185  frec2uzltd  9405  absext  9949  qabsor  9961  maxleast  10099  dvdslelemd  10243  odd2np1lem  10271  odd2np1  10272  isprm6  10526  bj-findis  10774