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

Theorem orim1d 814
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 23 . 2  |-  ( ph  ->  ( th  ->  th )
)
31, 2orim12d 813 1  |-  ( ph  ->  ( ( ps  \/  th )  ->  ( ch  \/  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 359
This theorem is referenced by:  pm2.38  817  pm2.73  820  pm2.74  821  pm2.8  825  pm2.82  827  moeq3  3113  unss1  3518  ordtri2or2  4680  gchor  8504  icombl  19460  ioombl  19461  relin01  25196  naim1  26136  onsucconi  26189  mblfinlem2  26246  leat3  30095  meetat2  30097  paddss1  30616
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 179  df-or 361  df-an 362
  Copyright terms: Public domain W3C validator