Theorem orim12d 776

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

Syntax hints:   -> wi 4   \/ wo 698

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orim1d  777  orim2d  778  3orim123d  1310  19.33b2  1617  eqifdc  3553  preq12b  3749  prel12  3750  exmidsssnc  4181  funun  5231  nnsucelsuc  6455  nnaord  6473  nnmord  6481  swoer  6525  fidceq  6831  fin0or  6848  enomnilem  7098  exmidomni  7102  fodjuomnilemres  7108  ltsopr  7533  cauappcvgprlemloc  7589  caucvgprlemloc  7612  caucvgprprlemloc  7640  suplocexprlemloc  7658  mulextsr1lem  7717  suplocsrlemb  7743  axpre-suploclemres  7838  reapcotr  8492  apcotr  8501  mulext1  8506  mulext  8508  mul0eqap  8563  peano2z  9223  zeo  9292  uzm1  9492  eluzdc  9544  fzospliti  10107  frec2uzltd  10334  absext  11001  qabsor  11013  maxleast  11151  dvdslelemd  11777  odd2np1lem  11805  odd2np1  11806  isprm6  12075  pythagtrip  12211  pc2dvds  12257  ennnfonelemrnh  12345  dedekindeulemloc  13197  suplociccreex  13202  dedekindicclemloc  13206  ivthinclemloc  13219  cos11  13374  lgsdir2lem4  13532  uzdcinzz  13639  bj-charfunr  13652  bj-findis  13821  nninfomnilem  13858  isomninnlem  13869