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  5314  nnsucelsuc  6576  nnaord  6594  nnmord  6602  swoer  6647  fidceq  6965  fin0or  6982  enomnilem  7239  exmidomni  7243  fodjuomnilemres  7249  ltsopr  7708  cauappcvgprlemloc  7764  caucvgprlemloc  7787  caucvgprprlemloc  7815  suplocexprlemloc  7833  mulextsr1lem  7892  suplocsrlemb  7918  axpre-suploclemres  8013  reapcotr  8670  apcotr  8679  mulext1  8684  mulext  8686  mul0eqap  8742  peano2z  9407  zeo  9477  uzm1  9678  eluzdc  9730  fzospliti  10298  frec2uzltd  10546  absext  11345  qabsor  11357  maxleast  11495  dvdslelemd  12125  odd2np1lem  12154  odd2np1  12155  isprm6  12440  pythagtrip  12577  pc2dvds  12624  ennnfonelemrnh  12758  aprcotr  14018  znidomb  14391  dedekindeulemloc  15062  suplociccreex  15067  dedekindicclemloc  15071  ivthinclemloc  15084  ivthdichlem  15094  plycj  15204  cos11  15296  lgsdir2lem4  15479  uzdcinzz  15696  bj-charfunr  15708  bj-findis  15877  nninfomnilem  15917  isomninnlem  15931