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

Theorem orim12i 503
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 382 . 2  |-  ( ph  ->  ( ps  \/  th ) )
3 orim12i.2 . . 3  |-  ( ch 
->  th )
43olcd 383 . 2  |-  ( ch 
->  ( ps  \/  th ) )
52, 4jaoi 369 1  |-  ( (
ph  \/  ch )  ->  ( ps  \/  th ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 358
This theorem is referenced by:  orim1i  504  orim2i  505  prlem2  930  eueq3  3052  pwssun  4430  xpima  5253  funcnvuni  5458  2oconcl  6683  fin23lem23  8139  fin23lem19  8149  fin1a2lem13  8225  fin1a2s  8227  ltadd2i  9136  nn0ge0  10179  mreexexd  13800  xpcbas  14202  odcl  15101  gexcl  15141  ang180lem4  20521  cusgrares  21347  2pthonlem2  21448  elim2ifim  23850  volmeas  24381  nepss  24954  funpsstri  25145  fvresval  25147  resolution  27883
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
  Copyright terms: Public domain W3C validator