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  1331  19.33b2  1640  eqifdc  3593  preq12b  3797  prel12  3798  exmidsssnc  4233  funun  5299  nnsucelsuc  6546  nnaord  6564  nnmord  6572  swoer  6617  fidceq  6927  fin0or  6944  enomnilem  7199  exmidomni  7203  fodjuomnilemres  7209  ltsopr  7658  cauappcvgprlemloc  7714  caucvgprlemloc  7737  caucvgprprlemloc  7765  suplocexprlemloc  7783  mulextsr1lem  7842  suplocsrlemb  7868  axpre-suploclemres  7963  reapcotr  8619  apcotr  8628  mulext1  8633  mulext  8635  mul0eqap  8691  peano2z  9356  zeo  9425  uzm1  9626  eluzdc  9678  fzospliti  10246  frec2uzltd  10477  absext  11210  qabsor  11222  maxleast  11360  dvdslelemd  11988  odd2np1lem  12016  odd2np1  12017  isprm6  12288  pythagtrip  12424  pc2dvds  12471  ennnfonelemrnh  12576  aprcotr  13784  znidomb  14157  dedekindeulemloc  14798  suplociccreex  14803  dedekindicclemloc  14807  ivthinclemloc  14820  ivthdichlem  14830  plycj  14939  cos11  15029  lgsdir2lem4  15188  uzdcinzz  15360  bj-charfunr  15372  bj-findis  15541  nninfomnilem  15578  isomninnlem  15590