Theorem orim12d 794

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 793	. 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 716

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1d  795  orim2d  796  3orim123d  1357  19.33b2  1678  eqifdc  3646  preq12b  3858  prel12  3859  exmidsssnc  4299  funun  5378  nnsucelsuc  6702  nnaord  6720  nnmord  6728  swoer  6773  fidceq  7099  fin0or  7118  fidcen  7131  enomnilem  7380  exmidomni  7384  fodjuomnilemres  7390  ltsopr  7859  cauappcvgprlemloc  7915  caucvgprlemloc  7938  caucvgprprlemloc  7966  suplocexprlemloc  7984  mulextsr1lem  8043  suplocsrlemb  8069  axpre-suploclemres  8164  reapcotr  8820  apcotr  8829  mulext1  8834  mulext  8836  mul0eqap  8892  peano2z  9559  zeo  9629  uzm1  9831  eluzdc  9888  fzospliti  10458  frec2uzltd  10711  absext  11686  qabsor  11698  maxleast  11836  dvdslelemd  12467  odd2np1lem  12496  odd2np1  12497  isprm6  12782  pythagtrip  12919  pc2dvds  12966  ennnfonelemrnh  13100  aprcotr  14364  znidomb  14737  dedekindeulemloc  15413  suplociccreex  15418  dedekindicclemloc  15422  ivthinclemloc  15435  ivthdichlem  15445  plycj  15555  cos11  15647  lgsdir2lem4  15833  uzdcinzz  16499  bj-charfunr  16509  bj-findis  16678  nninfomnilem  16727  isomninnlem  16745