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  961  eueq3  3278  pwssun  4786  xpima  5447  funcnvuni  6734  2oconcl  7150  fin23lem23  8702  fin23lem19  8712  fin1a2lem13  8788  fin1a2s  8790  ltadd2i  9711  nn0ge0  10817  hash2pwpr  12481  mreexexd  14899  xpcbas  15301  odcl  16356  gexcl  16396  ang180lem4  22872  cusgrares  24148  2pthlem2  24274  elim2ifim  27097  volmeas  27843  nepss  28570  funpsstri  28772  fvresval  28774  dvasin  29680  dvacos  29681  resolution  32295  bj-ifor  33239
  Copyright terms: Public domain W3C validator