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

Theorem orim12i 714
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 690 . 2  |-  ( ph  ->  ( ps  \/  th ) )
3 orim12i.2 . . 3  |-  ( ch 
->  th )
43olcd 691 . 2  |-  ( ch 
->  ( ps  \/  th ) )
52, 4jaoi 674 1  |-  ( (
ph  \/  ch )  ->  ( ps  \/  th ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 667
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  orim1i  715  orim2i  716  dcim  825  pm5.12dc  857  pm5.14dc  858  pm5.55dc  860  pm5.54dc  868  prlem2  923  xordc1  1336  19.43  1571  eueq3dc  2803  inssun  3255  abvor0dc  3325  ifmdc  3448  undifexmid  4049  pwssunim  4135  ordtriexmid  4366  ordtri2orexmid  4367  ontr2exmid  4369  onsucsssucexmid  4371  onsucelsucexmid  4374  ordsoexmid  4406  0elsucexmid  4409  ordpwsucexmid  4414  ordtri2or2exmid  4415  funcnvuni  5117  oprabidlem  5718  2oconcl  6241  inffiexmid  6702  unfiexmid  6708  djur  6837  djuun  6840  sup3exmid  8515  zeo  8950  ef0lem  11099
  Copyright terms: Public domain W3C validator