Theorem orim12d 788

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 787	. 2 |- ( ( ( ps -> ch ) /\ ( th -> ta ) ) -> ( ( ps \/ th ) -> ( ch \/ ta ) ) )
4	1, 2, 3	syl2anc 411	1 |- ( ph -> ( ( ps \/ th ) -> ( ch \/ ta ) ) )

Syntax hints:   -> wi 4   \/ wo 710

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1d  789  orim2d  790  3orim123d  1333  19.33b2  1653  eqifdc  3612  preq12b  3817  prel12  3818  exmidsssnc  4255  funun  5324  nnsucelsuc  6590  nnaord  6608  nnmord  6616  swoer  6661  fidceq  6981  fin0or  6998  enomnilem  7255  exmidomni  7259  fodjuomnilemres  7265  ltsopr  7729  cauappcvgprlemloc  7785  caucvgprlemloc  7808  caucvgprprlemloc  7836  suplocexprlemloc  7854  mulextsr1lem  7913  suplocsrlemb  7939  axpre-suploclemres  8034  reapcotr  8691  apcotr  8700  mulext1  8705  mulext  8707  mul0eqap  8763  peano2z  9428  zeo  9498  uzm1  9699  eluzdc  9751  fzospliti  10320  frec2uzltd  10570  absext  11449  qabsor  11461  maxleast  11599  dvdslelemd  12229  odd2np1lem  12258  odd2np1  12259  isprm6  12544  pythagtrip  12681  pc2dvds  12728  ennnfonelemrnh  12862  aprcotr  14122  znidomb  14495  dedekindeulemloc  15166  suplociccreex  15171  dedekindicclemloc  15175  ivthinclemloc  15188  ivthdichlem  15198  plycj  15308  cos11  15400  lgsdir2lem4  15583  uzdcinzz  15873  bj-charfunr  15884  bj-findis  16053  nninfomnilem  16096  isomninnlem  16110