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  8553  apcotr  8562  mulext1  8567  mulext  8569  mul0eqap  8625  peano2z  9287  zeo  9356  uzm1  9556  eluzdc  9608  fzospliti  10173  frec2uzltd  10400  absext  11067  qabsor  11079  maxleast  11217  dvdslelemd  11843  odd2np1lem  11871  odd2np1  11872  isprm6  12141  pythagtrip  12277  pc2dvds  12323  ennnfonelemrnh  12411  aprcotr  13336  dedekindeulemloc  14028  suplociccreex  14033  dedekindicclemloc  14037  ivthinclemloc  14050  cos11  14205  lgsdir2lem4  14363  uzdcinzz  14470  bj-charfunr  14482  bj-findis  14651  nninfomnilem  14687  isomninnlem  14698