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  2955  unss1  3357  ordtri2or2  4505  gchor  8265  icombl  18937  ioombl  18938  relin01  24104  naim1  24895  onsucconi  24948  untim2d  25124  leat3  30107  meetat2  30109  paddss1  30628
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