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

Theorem orim12i 760
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 734 . 2  |-  ( ph  ->  ( ps  \/  th ) )
3 orim12i.2 . . 3  |-  ( ch 
->  th )
43olcd 735 . 2  |-  ( ch 
->  ( ps  \/  th ) )
52, 4jaoi 717 1  |-  ( (
ph  \/  ch )  ->  ( ps  \/  th ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 709
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  orim1i  761  orim2i  762  dcim  842  pm5.12dc  911  pm5.14dc  912  pm5.55dc  914  pm5.54dc  919  prlem2  976  xordc1  1404  19.43  1639  eueq3dc  2926  inssun  3390  abvor0dc  3461  ifmdc  3589  undifexmid  4211  pwssunim  4302  ordtriexmid  4538  ontriexmidim  4539  ordtri2orexmid  4540  ontr2exmid  4542  onsucsssucexmid  4544  onsucelsucexmid  4547  ordsoexmid  4579  0elsucexmid  4582  ordpwsucexmid  4587  ordtri2or2exmid  4588  ontri2orexmidim  4589  funcnvuni  5304  oprabidlem  5926  2oconcl  6463  inffiexmid  6933  unfiexmid  6945  ctssexmid  7177  exmidonfinlem  7221  sup3exmid  8943  zeo  9387  ef0lem  11699
  Copyright terms: Public domain W3C validator