Theorem orim12d 787

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 786	. 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 709

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1d  788  orim2d  789  3orim123d  1332  19.33b2  1651  eqifdc  3606  preq12b  3810  prel12  3811  exmidsssnc  4246  funun  5312  nnsucelsuc  6567  nnaord  6585  nnmord  6593  swoer  6638  fidceq  6948  fin0or  6965  enomnilem  7222  exmidomni  7226  fodjuomnilemres  7232  ltsopr  7691  cauappcvgprlemloc  7747  caucvgprlemloc  7770  caucvgprprlemloc  7798  suplocexprlemloc  7816  mulextsr1lem  7875  suplocsrlemb  7901  axpre-suploclemres  7996  reapcotr  8653  apcotr  8662  mulext1  8667  mulext  8669  mul0eqap  8725  peano2z  9390  zeo  9460  uzm1  9661  eluzdc  9713  fzospliti  10281  frec2uzltd  10529  absext  11293  qabsor  11305  maxleast  11443  dvdslelemd  12073  odd2np1lem  12102  odd2np1  12103  isprm6  12388  pythagtrip  12525  pc2dvds  12572  ennnfonelemrnh  12706  aprcotr  13965  znidomb  14338  dedekindeulemloc  15009  suplociccreex  15014  dedekindicclemloc  15018  ivthinclemloc  15031  ivthdichlem  15041  plycj  15151  cos11  15243  lgsdir2lem4  15426  uzdcinzz  15598  bj-charfunr  15610  bj-findis  15779  nninfomnilem  15819  isomninnlem  15833