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  3571  preq12b  3772  prel12  3773  exmidsssnc  4205  funun  5262  nnsucelsuc  6494  nnaord  6512  nnmord  6520  swoer  6565  fidceq  6871  fin0or  6888  enomnilem  7138  exmidomni  7142  fodjuomnilemres  7148  ltsopr  7597  cauappcvgprlemloc  7653  caucvgprlemloc  7676  caucvgprprlemloc  7704  suplocexprlemloc  7722  mulextsr1lem  7781  suplocsrlemb  7807  axpre-suploclemres  7902  reapcotr  8557  apcotr  8566  mulext1  8571  mulext  8573  mul0eqap  8629  peano2z  9291  zeo  9360  uzm1  9560  eluzdc  9612  fzospliti  10178  frec2uzltd  10405  absext  11074  qabsor  11086  maxleast  11224  dvdslelemd  11851  odd2np1lem  11879  odd2np1  11880  isprm6  12149  pythagtrip  12285  pc2dvds  12331  ennnfonelemrnh  12419  aprcotr  13380  dedekindeulemloc  14136  suplociccreex  14141  dedekindicclemloc  14145  ivthinclemloc  14158  cos11  14313  lgsdir2lem4  14471  uzdcinzz  14589  bj-charfunr  14601  bj-findis  14770  nninfomnilem  14806  isomninnlem  14817