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  3640  preq12b  3851  prel12  3852  exmidsssnc  4291  funun  5368  nnsucelsuc  6654  nnaord  6672  nnmord  6680  swoer  6725  fidceq  7051  fin0or  7068  fidcen  7081  enomnilem  7328  exmidomni  7332  fodjuomnilemres  7338  ltsopr  7806  cauappcvgprlemloc  7862  caucvgprlemloc  7885  caucvgprprlemloc  7913  suplocexprlemloc  7931  mulextsr1lem  7990  suplocsrlemb  8016  axpre-suploclemres  8111  reapcotr  8768  apcotr  8777  mulext1  8782  mulext  8784  mul0eqap  8840  peano2z  9505  zeo  9575  uzm1  9777  eluzdc  9834  fzospliti  10403  frec2uzltd  10655  absext  11614  qabsor  11626  maxleast  11764  dvdslelemd  12394  odd2np1lem  12423  odd2np1  12424  isprm6  12709  pythagtrip  12846  pc2dvds  12893  ennnfonelemrnh  13027  aprcotr  14289  znidomb  14662  dedekindeulemloc  15333  suplociccreex  15338  dedekindicclemloc  15342  ivthinclemloc  15355  ivthdichlem  15365  plycj  15475  cos11  15567  lgsdir2lem4  15750  uzdcinzz  16330  bj-charfunr  16341  bj-findis  16510  nninfomnilem  16556  isomninnlem  16570