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

Theorem orim1d 837
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 836 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  840  pm2.73  843  pm2.74  844  pm2.8  848  pm2.82  850  moeq3  3285  unss1  3678  ordtri2or2  4980  gchor  9017  relin01  10089  icombl  21842  ioombl  21843  coltr  23879  frgraregorufrg  24896  naim1  29777  onsucconi  29829  mblfinlem2  29979  leat3  34493  meetat2  34495  paddss1  35014
  Copyright terms: Public domain W3C validator