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

Theorem orim12i 748
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 722 . 2  |-  ( ph  ->  ( ps  \/  th ) )
3 orim12i.2 . . 3  |-  ( ch 
->  th )
43olcd 723 . 2  |-  ( ch 
->  ( ps  \/  th ) )
52, 4jaoi 705 1  |-  ( (
ph  \/  ch )  ->  ( ps  \/  th ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 697
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  orim1i  749  orim2i  750  dcim  826  pm5.12dc  895  pm5.14dc  896  pm5.55dc  898  pm5.54dc  903  prlem2  958  xordc1  1371  19.43  1607  eueq3dc  2858  inssun  3316  abvor0dc  3386  ifmdc  3509  undifexmid  4117  pwssunim  4206  ordtriexmid  4437  ordtri2orexmid  4438  ontr2exmid  4440  onsucsssucexmid  4442  onsucelsucexmid  4445  ordsoexmid  4477  0elsucexmid  4480  ordpwsucexmid  4485  ordtri2or2exmid  4486  funcnvuni  5192  oprabidlem  5802  2oconcl  6336  inffiexmid  6800  unfiexmid  6806  ctssexmid  7024  exmidonfinlem  7049  sup3exmid  8722  zeo  9163  ef0lem  11373
  Copyright terms: Public domain W3C validator