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  2953  pwssun  4315  funcnvuni  5333  2oconcl  6518  fin23lem23  7968  fin23lem19  7978  fin1a2lem13  8054  fin1a2s  8056  ltadd2i  8966  nn0ge0  10007  mreexexd  13566  xpcbas  13968  odcl  14867  gexcl  14907  ang180lem4  20126  elim2ifim  23169  xpima  23217  nepss  24087  funpsstri  24192  fvresval  24194  condis  25045  condisd  25046  resolution  28518
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