Theorem orim12d 787

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 786	. 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 709

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1d  788  orim2d  789  3orim123d  1331  19.33b2  1643  eqifdc  3596  preq12b  3800  prel12  3801  exmidsssnc  4236  funun  5302  nnsucelsuc  6549  nnaord  6567  nnmord  6575  swoer  6620  fidceq  6930  fin0or  6947  enomnilem  7204  exmidomni  7208  fodjuomnilemres  7214  ltsopr  7663  cauappcvgprlemloc  7719  caucvgprlemloc  7742  caucvgprprlemloc  7770  suplocexprlemloc  7788  mulextsr1lem  7847  suplocsrlemb  7873  axpre-suploclemres  7968  reapcotr  8625  apcotr  8634  mulext1  8639  mulext  8641  mul0eqap  8697  peano2z  9362  zeo  9431  uzm1  9632  eluzdc  9684  fzospliti  10252  frec2uzltd  10495  absext  11228  qabsor  11240  maxleast  11378  dvdslelemd  12008  odd2np1lem  12037  odd2np1  12038  isprm6  12315  pythagtrip  12452  pc2dvds  12499  ennnfonelemrnh  12633  aprcotr  13841  znidomb  14214  dedekindeulemloc  14855  suplociccreex  14860  dedekindicclemloc  14864  ivthinclemloc  14877  ivthdichlem  14887  plycj  14997  cos11  15089  lgsdir2lem4  15272  uzdcinzz  15444  bj-charfunr  15456  bj-findis  15625  nninfomnilem  15662  isomninnlem  15674