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  6768  nnaord  6786  nnmord  6794  swoer  6839  fidceq  7175  fin0or  7194  fidcen  7207  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  9691  zeo  9762  uzm1  9969  eluzdc  10026  fzospliti  10602  frec2uzltd  10861  absext  11851  qabsor  11863  maxleast  12002  dvdslelemd  12635  odd2np1lem  12664  odd2np1  12665  isprm6  12951  nn0sqdcq  13013  sqrtrirr  13014  pythagtrip  13091  pc2dvds  13138  ennnfonelemrnh  13365  gsum2d2fi  14274  aprcotr  14706  znidomb  15102  dedekindeulemloc  15845  suplociccreex  15850  dedekindicclemloc  15854  ivthinclemloc  15867  ivthdichlem  15877  plycj  15987  cos11  16081  zprmlogbaplem2  16216  lgsdir2lem4  16355  uzdcinzz  17031  bj-charfunr  17041  bj-findis  17210  nninfomnilem  17267  isomninnlem  17285