Theorem orim12d 838

Description: Disjoin antecedents and consequents in a deduction. (Contributed by NM, 10-May-1994.)

Hypotheses

Ref	Expression
orim12d.1
orim12d.2

Assertion

Ref	Expression
orim12d

Proof of Theorem orim12d

Step	Hyp	Ref	Expression
1		orim12d.1	. 2
2		orim12d.2	. 2
3		pm3.48 833	. 2
4	1, 2, 3	syl2anc 661	1

Syntax hints:  ->wi 4  \/wo 368

This theorem is referenced by:  orim1d  839  orim2d  840  3orim123d  1307  preq12b  4206  prel12  4207  fr2nr  4862  ordtri3or  4915  sossfld  5459  funun  5635  soisores  6223  sorpsscmpl  6591  suceloni  6648  ordunisuc2  6679  fnse  6917  oaord  7215  omord2  7235  omcan  7237  oeord  7256  oecan  7257  nnaord  7287  nnmord  7300  omsmo  7322  swoer  7358  unxpwdom  8036  rankxplim3  8320  cdainflem  8592  ackbij2  8644  sornom  8678  fin23lem20  8738  fpwwe2lem10  9038  inatsk  9177  ltadd2  9709  ltord1  10104  ltmul1  10417  lt2msq  10454  xmullem2  11486  difreicc  11681  fzospliti  11857  om2uzlti  12061  om2uzlt2i  12062  om2uzf1oi  12064  absor  13133  ruclem12  13974  dvdslelem  14030  odd2np1lem  14045  odd2np1  14046  isprm6  14250  pythagtrip  14358  pc2dvds  14402  mreexexlem4d  15044  mreexexd  15045  irredrmul  17356  mplsubrglem  18100  mplsubrglemOLD  18101  znidomb  18600  ppttop  19508  filcon  20384  trufil  20411  ufildr  20432  plycj  22674  cosord  22919  logdivlt  23006  isosctrlem2  23153  atans2  23262  wilthlem2  23343  basellem3  23356  lgsdir2lem4  23601  pntpbnd1  23771  mirhl  24059  axcontlem2  24268  axcontlem4  24270  ex-natded5.13-2  25137  hiidge0  26015  chirredlem4  27312  ifbieq12d2  27420  disjxpin  27447  mul2lt0bi  27569  iocinif  27592  erdszelem11  28645  erdsze2lem2  28648  dfon2lem5  29219  trpredrec  29321  nofv  29417  btwnconn1lem14  29750  btwnconn2  29752  ispridlc  30467  rexzrexnn0  30737  pell14qrdich  30805  acongsym  30914  dvdsacongtr  30922  lcvexchlem4  34762  lcvexchlem5  34763  paddss1  35541  paddss2  35542

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