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

Theorem orim1d 835
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 24 . 2  |-  ( ph  ->  ( th  ->  th )
)
31, 2orim12d 834 1  |-  ( ph  ->  ( ( ps  \/  th )  ->  ( ch  \/  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 368
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
This theorem is referenced by:  pm2.38  838  pm2.73  841  pm2.74  842  pm2.8  846  pm2.82  848  moeq3  3134  unss1  3523  ordtri2or2  4813  gchor  8792  relin01  9862  icombl  21043  ioombl  21044  naim1  28229  onsucconi  28281  mblfinlem2  28426  frgraregorufrg  30662  leat3  32937  meetat2  32939  paddss1  33458
  Copyright terms: Public domain W3C validator