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  3663  preq12b  3879  prel12  3880  exmidsssnc  4321  funun  5402  nnsucelsuc  6737  nnaord  6755  nnmord  6763  swoer  6808  fidceq  7137  fin0or  7156  fidcen  7169  enomnilem  7442  exmidomni  7446  fodjuomnilemres  7452  ltsopr  7927  cauappcvgprlemloc  7983  caucvgprlemloc  8006  caucvgprprlemloc  8034  suplocexprlemloc  8052  mulextsr1lem  8111  suplocsrlemb  8137  axpre-suploclemres  8232  reapcotr  8889  apcotr  8898  mulext1  8903  mulext  8905  mul0eqap  8961  peano2z  9630  zeo  9701  uzm1  9903  eluzdc  9960  fzospliti  10534  frec2uzltd  10789  absext  11773  qabsor  11785  maxleast  11923  dvdslelemd  12554  odd2np1lem  12583  odd2np1  12584  isprm6  12869  pythagtrip  13006  pc2dvds  13053  ennnfonelemrnh  13251  aprcotr  14535  znidomb  14932  dedekindeulemloc  15610  suplociccreex  15615  dedekindicclemloc  15619  ivthinclemloc  15632  ivthdichlem  15642  plycj  15752  cos11  15844  lgsdir2lem4  16030  uzdcinzz  16696  bj-charfunr  16706  bj-findis  16875  nninfomnilem  16922  isomninnlem  16940