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

Theorem orim12i 502
Description: Disjoin antecedents and consequents of two premises. (Contributed by NM, 6-Jun-1994.) (Proof shortened by Wolf Lammen, 25-Jul-2012.)
Hypotheses
Ref Expression
orim12i.1  |-  ( ph  ->  ps )
orim12i.2  |-  ( ch 
->  th )
Assertion
Ref Expression
orim12i  |-  ( (
ph  \/  ch )  ->  ( ps  \/  th ) )

Proof of Theorem orim12i
StepHypRef Expression
1 orim12i.1 . . 3  |-  ( ph  ->  ps )
21orcd 381 . 2  |-  ( ph  ->  ( ps  \/  th ) )
3 orim12i.2 . . 3  |-  ( ch 
->  th )
43olcd 382 . 2  |-  ( ch 
->  ( ps  \/  th ) )
52, 4jaoi 368 1  |-  ( (
ph  \/  ch )  ->  ( ps  \/  th ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 357
This theorem is referenced by:  orim1i  503  orim2i  504  prlem2  929  eueq3  2940  pwssun  4299  funcnvuni  5317  2oconcl  6502  fin23lem23  7952  fin23lem19  7962  fin1a2lem13  8038  fin1a2s  8040  ltadd2i  8950  nn0ge0  9991  mreexexd  13550  xpcbas  13952  odcl  14851  gexcl  14891  ang180lem4  20110  elim2ifim  23153  xpima  23202  nepss  24072  funpsstri  24121  fvresval  24123  condis  24942  condisd  24943  resolution  28261
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
  Copyright terms: Public domain W3C validator