Theorem orim12d 791

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 790	. 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 713

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1d  792  orim2d  793  3orim123d  1354  19.33b2  1675  eqifdc  3639  preq12b  3848  prel12  3849  exmidsssnc  4287  funun  5362  nnsucelsuc  6637  nnaord  6655  nnmord  6663  swoer  6708  fidceq  7031  fin0or  7048  enomnilem  7305  exmidomni  7309  fodjuomnilemres  7315  ltsopr  7783  cauappcvgprlemloc  7839  caucvgprlemloc  7862  caucvgprprlemloc  7890  suplocexprlemloc  7908  mulextsr1lem  7967  suplocsrlemb  7993  axpre-suploclemres  8088  reapcotr  8745  apcotr  8754  mulext1  8759  mulext  8761  mul0eqap  8817  peano2z  9482  zeo  9552  uzm1  9753  eluzdc  9805  fzospliti  10374  frec2uzltd  10625  absext  11574  qabsor  11586  maxleast  11724  dvdslelemd  12354  odd2np1lem  12383  odd2np1  12384  isprm6  12669  pythagtrip  12806  pc2dvds  12853  ennnfonelemrnh  12987  aprcotr  14249  znidomb  14622  dedekindeulemloc  15293  suplociccreex  15298  dedekindicclemloc  15302  ivthinclemloc  15315  ivthdichlem  15325  plycj  15435  cos11  15527  lgsdir2lem4  15710  uzdcinzz  16162  bj-charfunr  16173  bj-findis  16342  nninfomnilem  16384  isomninnlem  16398