Theorem orim12d 798

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 797	. 2 |- ( ( ( ps -> ch ) /\ ( th -> ta ) ) -> ( ( ps \/ th ) -> ( ch \/ ta ) ) )
4	1, 2, 3	syl2anc 415	1 |- ( ph -> ( ( ps \/ th ) -> ( ch \/ ta ) ) )

Syntax hints:   -> wi 4   \/ wo 720

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 721

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1d  799  orim2d  800  3orim123d  1361  19.33b2  1682  eqifdc  3674  preq12b  3890  prel12  3891  exmidsssnc  4335  funun  5417  nnsucelsuc  6754  nnaord  6772  nnmord  6780  swoer  6825  fidceq  7161  fin0or  7180  fidcen  7193  enomnilem  7468  exmidomni  7472  fodjuomnilemres  7478  ltsopr  7953  cauappcvgprlemloc  8009  caucvgprlemloc  8032  caucvgprprlemloc  8060  suplocexprlemloc  8078  mulextsr1lem  8137  suplocsrlemb  8163  axpre-suploclemres  8258  reapcotr  8916  apcotr  8925  mulext1  8930  mulext  8932  mul0eqap  8990  peano2z  9659  zeo  9730  uzm1  9932  eluzdc  9989  fzospliti  10563  frec2uzltd  10818  absext  11807  qabsor  11819  maxleast  11957  dvdslelemd  12588  odd2np1lem  12617  odd2np1  12618  isprm6  12903  pythagtrip  13040  pc2dvds  13087  ennnfonelemrnh  13285  aprcotr  14570  znidomb  14965  dedekindeulemloc  15643  suplociccreex  15648  dedekindicclemloc  15652  ivthinclemloc  15665  ivthdichlem  15675  plycj  15785  cos11  15877  lgsdir2lem4  16064  uzdcinzz  16740  bj-charfunr  16750  bj-findis  16919  nninfomnilem  16966  isomninnlem  16984