MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orim12i Structured version   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  3101  pwssun  4481  xpima  5305  funcnvuni  5510  2oconcl  6739  fin23lem23  8198  fin23lem19  8208  fin1a2lem13  8284  fin1a2s  8286  ltadd2i  9196  nn0ge0  10239  mreexexd  13865  xpcbas  14267  odcl  15166  gexcl  15206  ang180lem4  20646  cusgrares  21473  2pthlem2  21588  elim2ifim  23998  volmeas  24579  nepss  25167  funpsstri  25381  fvresval  25383  resolution  28474
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