Theorem orim12d 781

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 780	. 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 703

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 704

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orim1d  782  orim2d  783  3orim123d  1315  19.33b2  1622  eqifdc  3560  preq12b  3757  prel12  3758  exmidsssnc  4189  funun  5242  nnsucelsuc  6470  nnaord  6488  nnmord  6496  swoer  6541  fidceq  6847  fin0or  6864  enomnilem  7114  exmidomni  7118  fodjuomnilemres  7124  ltsopr  7558  cauappcvgprlemloc  7614  caucvgprlemloc  7637  caucvgprprlemloc  7665  suplocexprlemloc  7683  mulextsr1lem  7742  suplocsrlemb  7768  axpre-suploclemres  7863  reapcotr  8517  apcotr  8526  mulext1  8531  mulext  8533  mul0eqap  8588  peano2z  9248  zeo  9317  uzm1  9517  eluzdc  9569  fzospliti  10132  frec2uzltd  10359  absext  11027  qabsor  11039  maxleast  11177  dvdslelemd  11803  odd2np1lem  11831  odd2np1  11832  isprm6  12101  pythagtrip  12237  pc2dvds  12283  ennnfonelemrnh  12371  dedekindeulemloc  13391  suplociccreex  13396  dedekindicclemloc  13400  ivthinclemloc  13413  cos11  13568  lgsdir2lem4  13726  uzdcinzz  13833  bj-charfunr  13845  bj-findis  14014  nninfomnilem  14051  isomninnlem  14062