Theorem orim12d 735

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 734	. 2 |- ( ( ( ps -> ch ) /\ ( th -> ta ) ) -> ( ( ps \/ th ) -> ( ch \/ ta ) ) )
4	1, 2, 3	syl2anc 403	1 |- ( ph -> ( ( ps \/ th ) -> ( ch \/ ta ) ) )

Syntax hints:   -> wi 4   \/ wo 664

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  orim1d  736  orim2d  737  3orim123d  1256  19.33b2  1565  eqifdc  3425  preq12b  3614  prel12  3615  funun  5058  nnsucelsuc  6252  nnaord  6268  nnmord  6276  swoer  6320  fidceq  6585  fin0or  6602  enomnilem  6794  exmidomni  6798  fodjuomnilemres  6803  ltsopr  7155  cauappcvgprlemloc  7211  caucvgprlemloc  7234  caucvgprprlemloc  7262  mulextsr1lem  7325  reapcotr  8075  apcotr  8084  mulext1  8089  mulext  8091  peano2z  8786  zeo  8851  uzm1  9049  eluzdc  9097  fzospliti  9587  frec2uzltd  9810  absext  10496  qabsor  10508  maxleast  10646  dvdslelemd  11122  odd2np1lem  11150  odd2np1  11151  isprm6  11404  uzdcinzz  11698  bj-findis  11874  nninfomnilem  11910