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

Theorem orim2d 814
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 22 . 2  |-  ( ph  ->  ( th  ->  th )
)
2 orim1d.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2orim12d 812 1  |-  ( ph  ->  ( ( th  \/  ps )  ->  ( th  \/  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 358
This theorem is referenced by:  orim2  815  pm2.82  826  poxp  6425  soxp  6426  nneo  10317  uzp1  10483  vdwlem9  13320  dfcon2  17443  fin1aufil  17925  dgrlt  20145  aalioulem2  20211  aalioulem5  20214  aalioulem6  20215  aaliou  20216  sqff1o  20926  disjpreima  23987  disjdsct  24051  voliune  24546  volfiniune  24547  relin01  25155  naim2  26047  lzunuz  26724  acongneg2  26940  paddss2  30312
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 178  df-or 360  df-an 361
  Copyright terms: Public domain W3C validator