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  1302  19.33b2  1609  eqifdc  3539  preq12b  3733  prel12  3734  exmidsssnc  4163  funun  5211  nnsucelsuc  6431  nnaord  6449  nnmord  6457  swoer  6501  fidceq  6807  fin0or  6824  enomnilem  7064  exmidomni  7068  fodjuomnilemres  7074  ltsopr  7499  cauappcvgprlemloc  7555  caucvgprlemloc  7578  caucvgprprlemloc  7606  suplocexprlemloc  7624  mulextsr1lem  7683  suplocsrlemb  7709  axpre-suploclemres  7804  reapcotr  8456  apcotr  8465  mulext1  8470  mulext  8472  mul0eqap  8527  peano2z  9186  zeo  9252  uzm1  9452  eluzdc  9503  fzospliti  10057  frec2uzltd  10284  absext  10945  qabsor  10957  maxleast  11095  dvdslelemd  11716  odd2np1lem  11744  odd2np1  11745  isprm6  12001  ennnfonelemrnh  12117  dedekindeulemloc  12957  suplociccreex  12962  dedekindicclemloc  12966  ivthinclemloc  12979  cos11  13134  uzdcinzz  13331  bj-charfunr  13344  bj-findis  13513  nninfomnilem  13552  isomninnlem  13563