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 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  837  orim2d  838  3orim123d  1306  preq12b  4187  prel12  4188  fr2nr  4843  ordtri3or  4896  sossfld  5440  funun  5616  soisores  6204  sorpsscmpl  6572  suceloni  6629  ordunisuc2  6660  fnse  6898  oaord  7194  omord2  7214  omcan  7216  oeord  7235  oecan  7236  nnaord  7266  nnmord  7279  omsmo  7301  swoer  7337  unxpwdom  8013  rankxplim3  8297  cdainflem  8569  ackbij2  8621  sornom  8655  fin23lem20  8715  fpwwe2lem10  9015  inatsk  9154  ltadd2  9686  ltord1  10080  ltmul1  10393  lt2msq  10430  xmullem2  11461  difreicc  11656  fzospliti  11831  om2uzlti  12035  om2uzlt2i  12036  om2uzf1oi  12038  absor  13107  ruclem12  13846  dvdslelem  13902  odd2np1lem  13917  odd2np1  13918  isprm6  14122  pythagtrip  14230  pc2dvds  14274  mreexexlem4d  14916  mreexexd  14917  irredrmul  17224  mplsubrglem  17968  mplsubrglemOLD  17969  znidomb  18467  ppttop  19374  filcon  20250  trufil  20277  ufildr  20298  plycj  22539  cosord  22784  logdivlt  22871  isosctrlem2  23018  atans2  23127  wilthlem2  23208  basellem3  23221  lgsdir2lem4  23466  pntpbnd1  23636  mirhl  23924  axcontlem2  24133  axcontlem4  24135  ex-natded5.13-2  25002  hiidge0  25880  chirredlem4  27177  ifbieq12d2  27285  disjxpin  27312  mul2lt0bi  27434  iocinif  27457  erdszelem11  28511  erdsze2lem2  28514  dfon2lem5  29187  trpredrec  29289  nofv  29385  btwnconn1lem14  29718  btwnconn2  29720  ispridlc  30435  rexzrexnn0  30705  pell14qrdich  30773  acongsym  30882  dvdsacongtr  30890  lcvexchlem4  34464  lcvexchlem5  34465  paddss1  35243  paddss2  35244