Theorem orim12d 786

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 785	. 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 708

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1d  787  orim2d  788  3orim123d  1320  19.33b2  1629  eqifdc  3569  preq12b  3769  prel12  3770  exmidsssnc  4201  funun  5257  nnsucelsuc  6487  nnaord  6505  nnmord  6513  swoer  6558  fidceq  6864  fin0or  6881  enomnilem  7131  exmidomni  7135  fodjuomnilemres  7141  ltsopr  7590  cauappcvgprlemloc  7646  caucvgprlemloc  7669  caucvgprprlemloc  7697  suplocexprlemloc  7715  mulextsr1lem  7774  suplocsrlemb  7800  axpre-suploclemres  7895  reapcotr  8549  apcotr  8558  mulext1  8563  mulext  8565  mul0eqap  8621  peano2z  9283  zeo  9352  uzm1  9552  eluzdc  9604  fzospliti  10169  frec2uzltd  10396  absext  11063  qabsor  11075  maxleast  11213  dvdslelemd  11839  odd2np1lem  11867  odd2np1  11868  isprm6  12137  pythagtrip  12273  pc2dvds  12319  ennnfonelemrnh  12407  aprcotr  13242  dedekindeulemloc  13879  suplociccreex  13884  dedekindicclemloc  13888  ivthinclemloc  13901  cos11  14056  lgsdir2lem4  14214  uzdcinzz  14321  bj-charfunr  14333  bj-findis  14502  nninfomnilem  14538  isomninnlem  14549