ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  orim12i Unicode version

Theorem orim12i 709
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 685 . 2  |-  ( ph  ->  ( ps  \/  th ) )
3 orim12i.2 . . 3  |-  ( ch 
->  th )
43olcd 686 . 2  |-  ( ch 
->  ( ps  \/  th ) )
52, 4jaoi 669 1  |-  ( (
ph  \/  ch )  ->  ( ps  \/  th ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 662
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  orim1i  710  orim2i  711  dcim  818  pm5.12dc  850  pm5.14dc  851  pm5.55dc  853  pm5.54dc  861  prlem2  916  xordc1  1325  19.43  1560  eueq3dc  2767  inssun  3211  abvor0dc  3276  pwssunim  4047  ordtriexmid  4273  ordtri2orexmid  4274  ontr2exmid  4276  onsucsssucexmid  4278  onsucelsucexmid  4281  ordsoexmid  4313  0elsucexmid  4316  ordpwsucexmid  4321  ordtri2or2exmid  4322  funcnvuni  4999  oprabidlem  5567  2oconcl  6086  unfiexmid  6438  zeo  8533
  Copyright terms: Public domain W3C validator