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  7478  exmidomni  7482  fodjuomnilemres  7488  ltsopr  7963  cauappcvgprlemloc  8019  caucvgprlemloc  8042  caucvgprprlemloc  8070  suplocexprlemloc  8088  mulextsr1lem  8147  suplocsrlemb  8173  axpre-suploclemres  8268  reapcotr  8928  apcotr  8937  mulext1  8942  mulext  8944  mul0eqap  9002  peano2z  9684  zeo  9755  uzm1  9962  eluzdc  10019  fzospliti  10595  frec2uzltd  10853  absext  11843  qabsor  11855  maxleast  11994  dvdslelemd  12626  odd2np1lem  12655  odd2np1  12656  isprm6  12942  nn0sqdcq  13004  sqrtrirr  13005  pythagtrip  13082  pc2dvds  13129  ennnfonelemrnh  13356  aprcotr  14646  znidomb  15042  dedekindeulemloc  15769  suplociccreex  15774  dedekindicclemloc  15778  ivthinclemloc  15791  ivthdichlem  15801  plycj  15911  cos11  16004  zprmlogbaplem2  16135  lgsdir2lem4  16248  uzdcinzz  16924  bj-charfunr  16934  bj-findis  17103  nninfomnilem  17159  isomninnlem  17177