Theorem orim12d 793

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 792	. 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 715

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1d  794  orim2d  795  3orim123d  1356  19.33b2  1677  eqifdc  3642  preq12b  3853  prel12  3854  exmidsssnc  4293  funun  5371  nnsucelsuc  6658  nnaord  6676  nnmord  6684  swoer  6729  fidceq  7055  fin0or  7074  fidcen  7087  enomnilem  7336  exmidomni  7340  fodjuomnilemres  7346  ltsopr  7815  cauappcvgprlemloc  7871  caucvgprlemloc  7894  caucvgprprlemloc  7922  suplocexprlemloc  7940  mulextsr1lem  7999  suplocsrlemb  8025  axpre-suploclemres  8120  reapcotr  8777  apcotr  8786  mulext1  8791  mulext  8793  mul0eqap  8849  peano2z  9514  zeo  9584  uzm1  9786  eluzdc  9843  fzospliti  10412  frec2uzltd  10664  absext  11623  qabsor  11635  maxleast  11773  dvdslelemd  12403  odd2np1lem  12432  odd2np1  12433  isprm6  12718  pythagtrip  12855  pc2dvds  12902  ennnfonelemrnh  13036  aprcotr  14298  znidomb  14671  dedekindeulemloc  15342  suplociccreex  15347  dedekindicclemloc  15351  ivthinclemloc  15364  ivthdichlem  15374  plycj  15484  cos11  15576  lgsdir2lem4  15759  uzdcinzz  16394  bj-charfunr  16405  bj-findis  16574  nninfomnilem  16620  isomninnlem  16634