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  1331  19.33b2  1640  eqifdc  3592  preq12b  3796  prel12  3797  exmidsssnc  4232  funun  5298  nnsucelsuc  6544  nnaord  6562  nnmord  6570  swoer  6615  fidceq  6925  fin0or  6942  enomnilem  7197  exmidomni  7201  fodjuomnilemres  7207  ltsopr  7656  cauappcvgprlemloc  7712  caucvgprlemloc  7735  caucvgprprlemloc  7763  suplocexprlemloc  7781  mulextsr1lem  7840  suplocsrlemb  7866  axpre-suploclemres  7961  reapcotr  8617  apcotr  8626  mulext1  8631  mulext  8633  mul0eqap  8689  peano2z  9353  zeo  9422  uzm1  9623  eluzdc  9675  fzospliti  10243  frec2uzltd  10474  absext  11207  qabsor  11219  maxleast  11357  dvdslelemd  11985  odd2np1lem  12013  odd2np1  12014  isprm6  12285  pythagtrip  12421  pc2dvds  12468  ennnfonelemrnh  12573  aprcotr  13781  znidomb  14146  dedekindeulemloc  14773  suplociccreex  14778  dedekindicclemloc  14782  ivthinclemloc  14795  ivthdichlem  14805  cos11  14988  lgsdir2lem4  15147  uzdcinzz  15290  bj-charfunr  15302  bj-findis  15471  nninfomnilem  15508  isomninnlem  15520