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  1643  eqifdc  3597  preq12b  3801  prel12  3802  exmidsssnc  4237  funun  5303  nnsucelsuc  6558  nnaord  6576  nnmord  6584  swoer  6629  fidceq  6939  fin0or  6956  enomnilem  7213  exmidomni  7217  fodjuomnilemres  7223  ltsopr  7680  cauappcvgprlemloc  7736  caucvgprlemloc  7759  caucvgprprlemloc  7787  suplocexprlemloc  7805  mulextsr1lem  7864  suplocsrlemb  7890  axpre-suploclemres  7985  reapcotr  8642  apcotr  8651  mulext1  8656  mulext  8658  mul0eqap  8714  peano2z  9379  zeo  9448  uzm1  9649  eluzdc  9701  fzospliti  10269  frec2uzltd  10512  absext  11245  qabsor  11257  maxleast  11395  dvdslelemd  12025  odd2np1lem  12054  odd2np1  12055  isprm6  12340  pythagtrip  12477  pc2dvds  12524  ennnfonelemrnh  12658  aprcotr  13917  znidomb  14290  dedekindeulemloc  14939  suplociccreex  14944  dedekindicclemloc  14948  ivthinclemloc  14961  ivthdichlem  14971  plycj  15081  cos11  15173  lgsdir2lem4  15356  uzdcinzz  15528  bj-charfunr  15540  bj-findis  15709  nninfomnilem  15749  isomninnlem  15761