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

Theorem orim2d 836
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
orim2d  |-  ( ph  ->  ( ( th  \/  ps )  ->  ( th  \/  ch ) ) )

Proof of Theorem orim2d
StepHypRef Expression
1 idd 24 . 2  |-  ( ph  ->  ( th  ->  th )
)
2 orim1d.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2orim12d 834 1  |-  ( ph  ->  ( ( th  \/  ps )  ->  ( th  \/  ch ) ) )
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:  orim2  837  pm2.82  848  poxp  6795  soxp  6796  relin01  9976  nneo  10837  uzp1  11006  vdwlem9  14169  dfcon2  19156  fin1aufil  19638  dgrlt  21867  aalioulem2  21933  aalioulem5  21936  aalioulem6  21937  aaliou  21938  sqff1o  22654  disjpreima  26080  disjdsct  26150  voliune  26790  volfiniune  26791  naim2  28377  lzunuz  29255  acongneg2  29469  paddss2  33801
  Copyright terms: Public domain W3C validator