Theorem orim12d 791

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

Syntax hints:   -> wi 4   \/ wo 713

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1d  792  orim2d  793  3orim123d  1354  19.33b2  1675  eqifdc  3639  preq12b  3848  prel12  3849  exmidsssnc  4287  funun  5362  nnsucelsuc  6645  nnaord  6663  nnmord  6671  swoer  6716  fidceq  7039  fin0or  7056  fidcen  7069  enomnilem  7316  exmidomni  7320  fodjuomnilemres  7326  ltsopr  7794  cauappcvgprlemloc  7850  caucvgprlemloc  7873  caucvgprprlemloc  7901  suplocexprlemloc  7919  mulextsr1lem  7978  suplocsrlemb  8004  axpre-suploclemres  8099  reapcotr  8756  apcotr  8765  mulext1  8770  mulext  8772  mul0eqap  8828  peano2z  9493  zeo  9563  uzm1  9765  eluzdc  9817  fzospliti  10386  frec2uzltd  10637  absext  11589  qabsor  11601  maxleast  11739  dvdslelemd  12369  odd2np1lem  12398  odd2np1  12399  isprm6  12684  pythagtrip  12821  pc2dvds  12868  ennnfonelemrnh  13002  aprcotr  14264  znidomb  14637  dedekindeulemloc  15308  suplociccreex  15313  dedekindicclemloc  15317  ivthinclemloc  15330  ivthdichlem  15340  plycj  15450  cos11  15542  lgsdir2lem4  15725  uzdcinzz  16217  bj-charfunr  16228  bj-findis  16397  nninfomnilem  16444  isomninnlem  16458