Theorem orim12d 856

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

Syntax hints:   -> wi 4   \/ wo 375

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 190  df-or 377  df-an 378

This theorem is referenced by:  orim1d  857  orim2d  858  3orim123d  1373  preq12b  4142  prel12  4143  fr2nr  4817  sossfld  5289  ordtri3or  5462  funun  5631  soisores  6236  sorpsscmpl  6601  suceloni  6659  ordunisuc2  6690  fnse  6932  oaord  7266  omord2  7286  omcan  7288  oeord  7307  oecan  7308  nnaord  7338  nnmord  7351  omsmo  7373  swoer  7409  unxpwdom  8122  rankxplim3  8370  cdainflem  8639  ackbij2  8691  sornom  8725  fin23lem20  8785  fpwwe2lem10  9082  inatsk  9221  ltadd2  9756  ltord1  10161  ltmul1  10477  lt2msq  10513  mul2lt0bi  11425  xmullem2  11576  difreicc  11790  fzospliti  11977  om2uzlti  12202  om2uzlt2i  12203  om2uzf1oi  12205  absor  13440  ruclem12  14370  dvdslelem  14426  odd2np1lem  14442  odd2np1  14443  isprm6  14745  pythagtrip  14863  pc2dvds  14907  mreexexlem4d  15631  mreexexd  15632  irredrmul  18013  mplsubrglem  18740  znidomb  19209  ppttop  20099  filcon  20976  trufil  21003  ufildr  21024  plycj  23310  cosord  23560  logdivlt  23649  isosctrlem2  23827  atans2  23936  wilthlem2  24073  basellem3  24088  lgsdir2lem4  24333  pntpbnd1  24503  mirhl  24803  axcontlem2  25074  axcontlem4  25076  ex-natded5.13-2  25945  hiidge0  26832  chirredlem4  28127  ifbieq12d2  28237  disjxpin  28275  iocinif  28438  erdszelem11  29996  erdsze2lem2  29999  dfon2lem5  30504  trpredrec  30550  nofv  30615  btwnconn1lem14  30938  btwnconn2  30940  poimir  32037  ispridlc  32367  lcvexchlem4  32674  lcvexchlem5  32675  paddss1  33453  paddss2  33454  rexzrexnn0  35718  pell14qrdich  35786  acongsym  35897  dvdsacongtr  35905  elmod2OLD  38871  propeqop  39146  nn0eo  40843