Theorem orim12d 787

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 786	. 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 709

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orim1d  788  orim2d  789  3orim123d  1332  19.33b2  1651  eqifdc  3606  preq12b  3810  prel12  3811  exmidsssnc  4246  funun  5314  nnsucelsuc  6576  nnaord  6594  nnmord  6602  swoer  6647  fidceq  6965  fin0or  6982  enomnilem  7239  exmidomni  7243  fodjuomnilemres  7249  ltsopr  7708  cauappcvgprlemloc  7764  caucvgprlemloc  7787  caucvgprprlemloc  7815  suplocexprlemloc  7833  mulextsr1lem  7892  suplocsrlemb  7918  axpre-suploclemres  8013  reapcotr  8670  apcotr  8679  mulext1  8684  mulext  8686  mul0eqap  8742  peano2z  9407  zeo  9477  uzm1  9678  eluzdc  9730  fzospliti  10298  frec2uzltd  10546  absext  11316  qabsor  11328  maxleast  11466  dvdslelemd  12096  odd2np1lem  12125  odd2np1  12126  isprm6  12411  pythagtrip  12548  pc2dvds  12595  ennnfonelemrnh  12729  aprcotr  13989  znidomb  14362  dedekindeulemloc  15033  suplociccreex  15038  dedekindicclemloc  15042  ivthinclemloc  15055  ivthdichlem  15065  plycj  15175  cos11  15267  lgsdir2lem4  15450  uzdcinzz  15667  bj-charfunr  15679  bj-findis  15848  nninfomnilem  15888  isomninnlem  15902