Theorem orim12d 850

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

Syntax hints:   -> wi 4   \/ wo 370

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 189  df-or 372  df-an 373

This theorem is referenced by:  orim1d  851  orim2d  852  3orim123d  1349  preq12b  4154  prel12  4155  fr2nr  4815  sossfld  5286  ordtri3or  5458  funun  5627  soisores  6223  sorpsscmpl  6587  suceloni  6645  ordunisuc2  6676  fnse  6918  oaord  7253  omord2  7273  omcan  7275  oeord  7294  oecan  7295  nnaord  7325  nnmord  7338  omsmo  7360  swoer  7396  unxpwdom  8109  rankxplim3  8357  cdainflem  8626  ackbij2  8678  sornom  8712  fin23lem20  8772  fpwwe2lem10  9069  inatsk  9208  ltadd2  9743  ltord1  10147  ltmul1  10462  lt2msq  10498  mul2lt0bi  11409  xmullem2  11558  difreicc  11771  fzospliti  11957  om2uzlti  12171  om2uzlt2i  12172  om2uzf1oi  12174  absor  13375  ruclem12  14305  dvdslelem  14361  odd2np1lem  14376  odd2np1  14377  isprm6  14678  pythagtrip  14796  pc2dvds  14840  mreexexlem4d  15565  mreexexd  15566  irredrmul  17947  mplsubrglem  18675  znidomb  19144  ppttop  20034  filcon  20910  trufil  20937  ufildr  20958  plycj  23243  cosord  23493  logdivlt  23582  isosctrlem2  23760  atans2  23869  wilthlem2  24006  basellem3  24021  lgsdir2lem4  24266  pntpbnd1  24436  mirhl  24736  axcontlem2  25007  axcontlem4  25009  ex-natded5.13-2  25878  hiidge0  26763  chirredlem4  28058  ifbieq12d2  28171  disjxpin  28210  iocinif  28375  erdszelem11  29936  erdsze2lem2  29939  dfon2lem5  30445  trpredrec  30491  nofv  30556  btwnconn1lem14  30879  btwnconn2  30881  poimir  31985  ispridlc  32315  lcvexchlem4  32615  lcvexchlem5  32616  paddss1  33394  paddss2  33395  rexzrexnn0  35659  pell14qrdich  35727  acongsym  35838  dvdsacongtr  35846  elmod2OLD  38736  propeqop  39009  nn0eo  40439