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  6659  nnaord  6677  nnmord  6685  swoer  6730  fidceq  7056  fin0or  7075  fidcen  7088  enomnilem  7337  exmidomni  7341  fodjuomnilemres  7347  ltsopr  7816  cauappcvgprlemloc  7872  caucvgprlemloc  7895  caucvgprprlemloc  7923  suplocexprlemloc  7941  mulextsr1lem  8000  suplocsrlemb  8026  axpre-suploclemres  8121  reapcotr  8778  apcotr  8787  mulext1  8792  mulext  8794  mul0eqap  8850  peano2z  9515  zeo  9585  uzm1  9787  eluzdc  9844  fzospliti  10413  frec2uzltd  10666  absext  11641  qabsor  11653  maxleast  11791  dvdslelemd  12422  odd2np1lem  12451  odd2np1  12452  isprm6  12737  pythagtrip  12874  pc2dvds  12921  ennnfonelemrnh  13055  aprcotr  14318  znidomb  14691  dedekindeulemloc  15362  suplociccreex  15367  dedekindicclemloc  15371  ivthinclemloc  15384  ivthdichlem  15394  plycj  15504  cos11  15596  lgsdir2lem4  15779  uzdcinzz  16445  bj-charfunr  16456  bj-findis  16625  nninfomnilem  16671  isomninnlem  16685