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 ) ) )

This proof depends on syntax axioms:   -> wi 4   \/ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  orim1d  799  orim2d  800  3orim123d  1361  19.33b2  1682  eqifdc  3677  preq12b  3895  prel12  3896  exmidsssnc  4340  funun  5422  nnsucelsuc  6764  nnaord  6782  nnmord  6790  swoer  6835  fidceq  7171  fin0or  7190  fidcen  7203  enomnilem  7478  exmidomni  7482  fodjuomnilemres  7488  ltsopr  7963  cauappcvgprlemloc  8019  caucvgprlemloc  8042  caucvgprprlemloc  8070  suplocexprlemloc  8088  mulextsr1lem  8147  suplocsrlemb  8173  axpre-suploclemres  8268  reapcotr  8926  apcotr  8935  mulext1  8940  mulext  8942  mul0eqap  9000  peano2z  9680  zeo  9751  uzm1  9953  eluzdc  10010  fzospliti  10585  frec2uzltd  10840  absext  11829  qabsor  11841  maxleast  11979  dvdslelemd  12610  odd2np1lem  12639  odd2np1  12640  isprm6  12925  pythagtrip  13062  pc2dvds  13109  ennnfonelemrnh  13307  aprcotr  14597  znidomb  14993  dedekindeulemloc  15720  suplociccreex  15725  dedekindicclemloc  15729  ivthinclemloc  15742  ivthdichlem  15752  plycj  15862  cos11  15954  lgsdir2lem4  16150  uzdcinzz  16826  bj-charfunr  16836  bj-findis  17005  nninfomnilem  17061  isomninnlem  17079