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

Theorem orim2d 813
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 21 . 2  |-  ( ph  ->  ( th  ->  th )
)
2 orim1d.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2orim12d 811 1  |-  ( ph  ->  ( ( th  \/  ps )  ->  ( th  \/  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 357
This theorem is referenced by:  orim2  814  pm2.82  825  poxp  6311  soxp  6312  nneo  10184  uzp1  10350  vdwlem9  13127  dfcon2  17245  fin1aufil  17723  dgrlt  19745  aalioulem2  19811  aalioulem5  19814  aalioulem6  19815  aaliou  19816  sqff1o  20526  disjpreima  23222  disjdsct  23291  voliune  23849  volfiniune  23850  relin01  24495  naim2  25383  lzunuz  26170  acongneg2  26387  paddss2  30059
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360
  Copyright terms: Public domain W3C validator