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

Theorem orim12i 514
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 390 . 2  |-  ( ph  ->  ( ps  \/  th ) )
3 orim12i.2 . . 3  |-  ( ch 
->  th )
43olcd 391 . 2  |-  ( ch 
->  ( ps  \/  th ) )
52, 4jaoi 377 1  |-  ( (
ph  \/  ch )  ->  ( ps  \/  th ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 366
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 368
This theorem is referenced by:  orim1i  515  orim2i  516  prlem2  961  eueq3  3271  pwssun  4775  xpima  5434  funcnvuni  6726  2oconcl  7145  fin23lem23  8697  fin23lem19  8707  fin1a2lem13  8783  fin1a2s  8785  ltadd2iOLD  9705  nn0ge0  10817  hash2pwpr  12506  trclfvg  12936  mreexexd  15140  xpcbas  15649  odcl  16762  gexcl  16802  ang180lem4  23346  cusgrares  24677  2pthlem2  24803  elim2ifim  27632  locfinref  28082  volmeas  28443  nepss  29339  funpsstri  29439  fvresval  29441  dvasin  30346  dvacos  30347  resolution  33621  ifpor  34579  relexpxpmin  38247
  Copyright terms: Public domain W3C validator