Theorem orim12d 798

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

This proof depends on syntax axioms:   -> wi 4   \/ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  orim1d  799  orim2d  800  3orim123d  1361  19.33b2  1682  eqifdc  3677  preq12b  3895  prel12  3896  exmidsssnc  4342  funun  5425  nnsucelsuc  6769  nnaord  6787  nnmord  6795  swoer  6840  fidceq  7177  fin0or  7196  fidcen  7209  enomnilem  7484  exmidomni  7488  fodjuomnilemres  7494  ltsopr  7969  cauappcvgprlemloc  8025  caucvgprlemloc  8048  caucvgprprlemloc  8076  suplocexprlemloc  8094  mulextsr1lem  8153  suplocsrlemb  8179  axpre-suploclemres  8274  reapcotr  8934  apcotr  8943  mulext1  8948  mulext  8950  mul0eqap  9008  peano2z  9689  zeo  9761  uzm1  9968  eluzdc  10025  fzospliti  10601  frec2uzltd  10860  absext  11850  qabsor  11862  maxleast  12001  dvdslelemd  12634  odd2np1lem  12663  odd2np1  12664  isprm6  12950  nn0sqdcq  13012  sqrtrirr  13013  pythagtrip  13090  pc2dvds  13137  ennnfonelemrnh  13364  gsum2d2fi  14273  aprcotr  14705  znidomb  15101  dedekindeulemloc  15862  suplociccreex  15867  dedekindicclemloc  15871  ivthinclemloc  15884  ivthdichlem  15894  plycj  16004  cos11  16098  zprmlogbaplem2  16233  lgsdir2lem4  16372  uzdcinzz  17048  bj-charfunr  17058  bj-findis  17227  nninfomnilem  17284  isomninnlem  17302