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

Theorem orim2d 840
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 838 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  841  pm2.82  852  poxp  6911  soxp  6912  relin01  10098  nneo  10967  uzp1  11139  vdwlem9  14518  dfcon2  20045  fin1aufil  20558  dgrlt  22788  aalioulem2  22854  aalioulem5  22857  aalioulem6  22858  aaliou  22859  sqff1o  23581  disjpreima  27582  disjdsct  27669  voliune  28362  volfiniune  28363  naim2  30013  lzunuz  30863  acongneg2  31077  paddss2  35643
  Copyright terms: Public domain W3C validator