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

Theorem orim1d 812
Description: Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
Hypothesis
Ref Expression
orim1d.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
orim1d  |-  ( ph  ->  ( ( ps  \/  th )  ->  ( ch  \/  th ) ) )

Proof of Theorem orim1d
StepHypRef Expression
1 orim1d.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 idd 21 . 2  |-  ( ph  ->  ( th  ->  th )
)
31, 2orim12d 811 1  |-  ( ph  ->  ( ( ps  \/  th )  ->  ( ch  \/  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 357
This theorem is referenced by:  pm2.38  815  pm2.73  818  pm2.74  819  pm2.8  823  pm2.82  825  moeq3  2942  unss1  3344  ordtri2or2  4489  gchor  8249  icombl  18921  ioombl  18922  relin01  24089  naim1  24823  onsucconi  24876  untim2d  25021  leat3  29485  meetat2  29487  paddss1  30006
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360
  Copyright terms: Public domain W3C validator