Theorem orim12d 883

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

Syntax hints:   -> wi 4   \/ wo 383

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 197  df-or 385  df-an 386

This theorem is referenced by:  orim1d  884  orim2d  885  3orim123d  1407  preq12b  4382  prel12  4383  propeqop  4970  fr2nr  5092  sossfld  5580  ordtri3or  5755  ordelinel  5825  funun  5932  soisores  6577  sorpsscmpl  6948  suceloni  7013  ordunisuc2  7044  fnse  7294  oaord  7627  omord2  7647  omcan  7649  oeord  7668  oecan  7669  nnaord  7699  nnmord  7712  omsmo  7734  swoer  7772  unxpwdom  8494  rankxplim3  8744  cdainflem  9013  ackbij2  9065  sornom  9099  fin23lem20  9159  fpwwe2lem10  9461  inatsk  9600  ltadd2  10141  ltord1  10554  ltmul1  10873  lt2msq  10908  mul2lt0bi  11936  xmullem2  12095  difreicc  12304  fzospliti  12500  om2uzlti  12749  om2uzlt2i  12750  om2uzf1oi  12752  absor  14040  ruclem12  14970  dvdslelem  15031  odd2np1lem  15064  odd2np1  15065  isprm6  15426  pythagtrip  15539  pc2dvds  15583  mreexexlem4d  16307  mreexexd  16308  mreexexdOLD  16309  irredrmul  18707  mplsubrglem  19439  znidomb  19910  ppttop  20811  filconn  21687  trufil  21714  ufildr  21735  plycj  24033  cosord  24278  logdivlt  24367  isosctrlem2  24549  atans2  24658  wilthlem2  24795  basellem3  24809  lgsdir2lem4  25053  pntpbnd1  25275  mirhl  25574  axcontlem2  25845  axcontlem4  25847  ex-natded5.13-2  27273  hiidge0  27955  chirredlem4  29252  disjxpin  29401  iocinif  29543  erdszelem11  31183  erdsze2lem2  31186  dfon2lem5  31692  trpredrec  31738  nofv  31810  nolesgn2o  31824  btwnconn1lem14  32207  btwnconn2  32209  poimir  33442  ispridlc  33869  lcvexchlem4  34324  lcvexchlem5  34325  paddss1  35103  paddss2  35104  rexzrexnn0  37368  pell14qrdich  37433  acongsym  37543  dvdsacongtr  37551  or3or  38319  clsk1indlem3  38341  nn0eo  42322