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

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

Proof of Theorem orim1d
StepHypRef Expression
1 orim1d.1 . 2
2 idd 24 . 2
31, 2orim12d 838 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  \/wo 368
This theorem is referenced by:  pm2.38  842  pm2.73  845  pm2.74  846  pm2.8  850  pm2.82  852  moeq3  3276  unss1  3672  ordtri2or2  4979  gchor  9026  relin01  10102  icombl  21974  ioombl  21975  coltr  24027  frgraregorufrg  25072  naim1  29850  onsucconi  29902  mblfinlem2  30052  leat3  35020  meetat2  35022  paddss1  35541
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