Theorem orim12d 776

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

Syntax hints:   -> wi 4   \/ wo 698

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orim1d  777  orim2d  778  3orim123d  1299  19.33b2  1609  eqifdc  3511  preq12b  3705  prel12  3706  exmidsssnc  4134  funun  5175  nnsucelsuc  6395  nnaord  6413  nnmord  6421  swoer  6465  fidceq  6771  fin0or  6788  enomnilem  7018  exmidomni  7022  fodjuomnilemres  7028  ltsopr  7428  cauappcvgprlemloc  7484  caucvgprlemloc  7507  caucvgprprlemloc  7535  suplocexprlemloc  7553  mulextsr1lem  7612  suplocsrlemb  7638  axpre-suploclemres  7733  reapcotr  8384  apcotr  8393  mulext1  8398  mulext  8400  mul0eqap  8455  peano2z  9114  zeo  9180  uzm1  9380  eluzdc  9431  fzospliti  9984  frec2uzltd  10207  absext  10867  qabsor  10879  maxleast  11017  dvdslelemd  11577  odd2np1lem  11605  odd2np1  11606  isprm6  11861  ennnfonelemrnh  11965  dedekindeulemloc  12805  suplociccreex  12810  dedekindicclemloc  12814  ivthinclemloc  12827  cos11  12982  uzdcinzz  13176  bj-findis  13348  nninfomnilem  13389  isomninnlem  13400