Theorem orim12d 836

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

Syntax hints:   -> wi 4   \/ wo 366

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 368  df-an 369

This theorem is referenced by:  orim1d  837  orim2d  838  3orim123d  1305  preq12b  4137  prel12  4138  fr2nr  4788  ordtri3or  4841  sossfld  5380  funun  5555  soisores  6146  sorpsscmpl  6512  suceloni  6569  ordunisuc2  6600  fnse  6838  oaord  7136  omord2  7156  omcan  7158  oeord  7177  oecan  7178  nnaord  7208  nnmord  7221  omsmo  7243  swoer  7279  unxpwdom  7952  rankxplim3  8234  cdainflem  8506  ackbij2  8558  sornom  8592  fin23lem20  8652  fpwwe2lem10  8950  inatsk  9089  ltadd2  9621  ltord1  10018  ltmul1  10331  lt2msq  10367  xmullem2  11400  difreicc  11595  fzospliti  11774  om2uzlti  11987  om2uzlt2i  11988  om2uzf1oi  11990  absor  13158  ruclem12  13999  dvdslelem  14055  odd2np1lem  14070  odd2np1  14071  isprm6  14275  pythagtrip  14383  pc2dvds  14427  mreexexlem4d  15077  mreexexd  15078  irredrmul  17492  mplsubrglem  18236  mplsubrglemOLD  18237  znidomb  18714  ppttop  19616  filcon  20492  trufil  20519  ufildr  20540  plycj  22782  cosord  23027  logdivlt  23116  isosctrlem2  23292  atans2  23401  wilthlem2  23483  basellem3  23496  lgsdir2lem4  23741  pntpbnd1  23911  mirhl  24204  axcontlem2  24414  axcontlem4  24416  ex-natded5.13-2  25283  hiidge0  26157  chirredlem4  27453  ifbieq12d2  27572  disjxpin  27611  mul2lt0bi  27753  iocinif  27779  erdszelem11  28874  erdsze2lem2  28877  dfon2lem5  29424  trpredrec  29526  nofv  29622  btwnconn1lem14  29943  btwnconn2  29945  ispridlc  30673  rexzrexnn0  30943  pell14qrdich  31010  acongsym  31119  dvdsacongtr  31127  elmod2OLD  32502  nn0eo  33384  lcvexchlem4  35214  lcvexchlem5  35215  paddss1  35993  paddss2  35994