Theorem orim12d 794

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 793	. 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 716

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1d  795  orim2d  796  3orim123d  1357  19.33b2  1678  eqifdc  3659  preq12b  3874  prel12  3875  exmidsssnc  4316  funun  5397  nnsucelsuc  6724  nnaord  6742  nnmord  6750  swoer  6795  fidceq  7124  fin0or  7143  fidcen  7156  enomnilem  7429  exmidomni  7433  fodjuomnilemres  7439  ltsopr  7911  cauappcvgprlemloc  7967  caucvgprlemloc  7990  caucvgprprlemloc  8018  suplocexprlemloc  8036  mulextsr1lem  8095  suplocsrlemb  8121  axpre-suploclemres  8216  reapcotr  8872  apcotr  8881  mulext1  8886  mulext  8888  mul0eqap  8944  peano2z  9613  zeo  9683  uzm1  9885  eluzdc  9942  fzospliti  10512  frec2uzltd  10765  absext  11748  qabsor  11760  maxleast  11898  dvdslelemd  12529  odd2np1lem  12558  odd2np1  12559  isprm6  12844  pythagtrip  12981  pc2dvds  13028  ennnfonelemrnh  13167  aprcotr  14431  znidomb  14806  dedekindeulemloc  15484  suplociccreex  15489  dedekindicclemloc  15493  ivthinclemloc  15506  ivthdichlem  15516  plycj  15626  cos11  15718  lgsdir2lem4  15904  uzdcinzz  16570  bj-charfunr  16580  bj-findis  16749  nninfomnilem  16796  isomninnlem  16814