MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orim2d Unicode version

Theorem orim2d 840
Description: Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
Hypothesis
Ref Expression
orim1d.1
Assertion
Ref Expression
orim2d

Proof of Theorem orim2d
StepHypRef Expression
1 idd 24 . 2
2 orim1d.1 . 2
31, 2orim12d 838 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  \/wo 368
This theorem is referenced by:  orim2  841  pm2.82  852  poxp  6912  soxp  6913  relin01  10102  nneo  10971  uzp1  11143  vdwlem9  14507  dfcon2  19920  fin1aufil  20433  dgrlt  22663  aalioulem2  22729  aalioulem5  22732  aalioulem6  22733  aaliou  22734  sqff1o  23456  disjpreima  27445  disjdsct  27521  voliune  28201  volfiniune  28202  naim2  29851  lzunuz  30701  acongneg2  30915  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
  Copyright terms: Public domain W3C validator