Theorem orim12d 834

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

Syntax hints:   -> wi 4   \/ wo 368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371

This theorem is referenced by:  orim1d  835  orim2d  836  3orim123d  1297  preq12b  4046  prel12  4047  fr2nr  4696  ordtri3or  4749  sossfld  5283  funun  5458  soisores  6016  sorpsscmpl  6369  suceloni  6422  ordunisuc2  6453  fnse  6687  oaord  6984  omord2  7004  omcan  7006  oeord  7025  oecan  7026  nnaord  7056  nnmord  7069  omsmo  7091  swoer  7127  unxpwdom  7802  rankxplim3  8086  cdainflem  8358  ackbij2  8410  sornom  8444  fin23lem20  8504  fpwwe2lem10  8804  inatsk  8943  ltadd2  9476  ltord1  9864  ltmul1  10177  lt2msq  10214  xmullem2  11226  difreicc  11415  fzospliti  11579  om2uzlti  11771  om2uzlt2i  11772  om2uzf1oi  11774  absor  12787  ruclem12  13521  dvdslelem  13575  odd2np1lem  13589  odd2np1  13590  isprm6  13793  pythagtrip  13899  pc2dvds  13943  mreexexlem4d  14583  mreexexd  14584  irredrmul  16797  mplsubrglem  17515  mplsubrglemOLD  17516  znidomb  17992  ppttop  18609  filcon  19454  trufil  19481  ufildr  19502  plycj  21742  cosord  21986  logdivlt  22068  isosctrlem2  22215  atans2  22324  wilthlem2  22405  basellem3  22418  lgsdir2lem4  22663  pntpbnd1  22833  ncolne2  23031  axcontlem2  23209  axcontlem4  23211  ex-natded5.13-2  23621  hiidge0  24498  chirredlem4  25795  ifbieq12d2  25901  disjxpin  25928  mul2lt0bi  26040  iocinif  26069  erdszelem11  27087  erdsze2lem2  27090  dfon2lem5  27598  trpredrec  27700  nofv  27796  btwnconn1lem14  28129  btwnconn2  28131  ispridlc  28867  rexzrexnn0  29139  pell14qrdich  29207  acongsym  29316  dvdsacongtr  29324  lcvexchlem4  32679  lcvexchlem5  32680  paddss1  33458  paddss2  33459