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  3847  prel12  3848  exmidsssnc  4286  funun  5361  nnsucelsuc  6635  nnaord  6653  nnmord  6661  swoer  6706  fidceq  7027  fin0or  7044  enomnilem  7301  exmidomni  7305  fodjuomnilemres  7311  ltsopr  7779  cauappcvgprlemloc  7835  caucvgprlemloc  7858  caucvgprprlemloc  7886  suplocexprlemloc  7904  mulextsr1lem  7963  suplocsrlemb  7989  axpre-suploclemres  8084  reapcotr  8741  apcotr  8750  mulext1  8755  mulext  8757  mul0eqap  8813  peano2z  9478  zeo  9548  uzm1  9749  eluzdc  9801  fzospliti  10370  frec2uzltd  10620  absext  11569  qabsor  11581  maxleast  11719  dvdslelemd  12349  odd2np1lem  12378  odd2np1  12379  isprm6  12664  pythagtrip  12801  pc2dvds  12848  ennnfonelemrnh  12982  aprcotr  14243  znidomb  14616  dedekindeulemloc  15287  suplociccreex  15292  dedekindicclemloc  15296  ivthinclemloc  15309  ivthdichlem  15319  plycj  15429  cos11  15521  lgsdir2lem4  15704  uzdcinzz  16120  bj-charfunr  16131  bj-findis  16300  nninfomnilem  16343  isomninnlem  16357