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

Theorem orim12i 516
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 392 . 2  |-  ( ph  ->  ( ps  \/  th ) )
3 orim12i.2 . . 3  |-  ( ch 
->  th )
43olcd 393 . 2  |-  ( ch 
->  ( ps  \/  th ) )
52, 4jaoi 379 1  |-  ( (
ph  \/  ch )  ->  ( ps  \/  th ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 368
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-or 370
This theorem is referenced by:  orim1i  517  orim2i  518  prlem2  954  eueq3  3217  pwssun  4711  xpima  5364  funcnvuni  6616  2oconcl  7029  fin23lem23  8582  fin23lem19  8592  fin1a2lem13  8668  fin1a2s  8670  ltadd2i  9592  nn0ge0  10692  hash2pwpr  12270  mreexexd  14674  xpcbas  15076  odcl  16129  gexcl  16169  ang180lem4  22310  cusgrares  23501  2pthlem2  23616  elim2ifim  26027  volmeas  26767  nepss  27494  funpsstri  27696  fvresval  27698  dvasin  28604  dvacos  28605  resolution  31433  bj-ifor  32377
  Copyright terms: Public domain W3C validator