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  3770  prel12  3771  exmidsssnc  4203  funun  5260  nnsucelsuc  6491  nnaord  6509  nnmord  6517  swoer  6562  fidceq  6868  fin0or  6885  enomnilem  7135  exmidomni  7139  fodjuomnilemres  7145  ltsopr  7594  cauappcvgprlemloc  7650  caucvgprlemloc  7673  caucvgprprlemloc  7701  suplocexprlemloc  7719  mulextsr1lem  7778  suplocsrlemb  7804  axpre-suploclemres  7899  reapcotr  8554  apcotr  8563  mulext1  8568  mulext  8570  mul0eqap  8626  peano2z  9288  zeo  9357  uzm1  9557  eluzdc  9609  fzospliti  10175  frec2uzltd  10402  absext  11071  qabsor  11083  maxleast  11221  dvdslelemd  11848  odd2np1lem  11876  odd2np1  11877  isprm6  12146  pythagtrip  12282  pc2dvds  12328  ennnfonelemrnh  12416  aprcotr  13373  dedekindeulemloc  14067  suplociccreex  14072  dedekindicclemloc  14076  ivthinclemloc  14089  cos11  14244  lgsdir2lem4  14402  uzdcinzz  14520  bj-charfunr  14532  bj-findis  14701  nninfomnilem  14737  isomninnlem  14748