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

Theorem orim2d 815
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 23 . 2  |-  ( ph  ->  ( th  ->  th )
)
2 orim1d.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2orim12d 813 1  |-  ( ph  ->  ( ( th  \/  ps )  ->  ( th  \/  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 359
This theorem is referenced by:  orim2  816  pm2.82  827  poxp  6487  soxp  6488  nneo  10384  uzp1  10550  vdwlem9  13388  dfcon2  17513  fin1aufil  17995  dgrlt  20215  aalioulem2  20281  aalioulem5  20284  aalioulem6  20285  aaliou  20286  sqff1o  20996  disjpreima  24057  disjdsct  24121  voliune  24616  volfiniune  24617  relin01  25225  naim2  26166  lzunuz  26864  acongneg2  27080  paddss2  30713
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 179  df-or 361  df-an 362
  Copyright terms: Public domain W3C validator