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  4340  funun  5422  nnsucelsuc  6764  nnaord  6782  nnmord  6790  swoer  6835  fidceq  7171  fin0or  7190  fidcen  7203  enomnilem  7479  exmidomni  7483  fodjuomnilemres  7489  ltsopr  7964  cauappcvgprlemloc  8020  caucvgprlemloc  8043  caucvgprprlemloc  8071  suplocexprlemloc  8089  mulextsr1lem  8148  suplocsrlemb  8174  axpre-suploclemres  8269  reapcotr  8929  apcotr  8938  mulext1  8943  mulext  8945  mul0eqap  9003  peano2z  9685  zeo  9756  uzm1  9963  eluzdc  10020  fzospliti  10596  frec2uzltd  10855  absext  11845  qabsor  11857  maxleast  11996  dvdslelemd  12629  odd2np1lem  12658  odd2np1  12659  isprm6  12945  nn0sqdcq  13007  sqrtrirr  13008  pythagtrip  13085  pc2dvds  13132  ennnfonelemrnh  13359  aprcotr  14681  znidomb  15077  dedekindeulemloc  15811  suplociccreex  15816  dedekindicclemloc  15820  ivthinclemloc  15833  ivthdichlem  15843  plycj  15953  cos11  16046  zprmlogbaplem2  16177  lgsdir2lem4  16316  uzdcinzz  16992  bj-charfunr  17002  bj-findis  17171  nninfomnilem  17227  isomninnlem  17245