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

Theorem orim12i 676
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 (𝜑𝜓)
orim12i.2 (𝜒𝜃)
Assertion
Ref Expression
orim12i ((𝜑𝜒) → (𝜓𝜃))

Proof of Theorem orim12i
StepHypRef Expression
1 orim12i.1 . . 3 (𝜑𝜓)
21orcd 652 . 2 (𝜑 → (𝜓𝜃))
3 orim12i.2 . . 3 (𝜒𝜃)
43olcd 653 . 2 (𝜒 → (𝜓𝜃))
52, 4jaoi 636 1 ((𝜑𝜒) → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wo 629
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  orim1i  677  orim2i  678  dcim  784  pm5.12dc  816  pm5.14dc  817  pm5.55dc  819  pm5.54dc  827  prlem2  881  xordc1  1284  19.43  1519  eueq3dc  2715  inssun  3177  abvor0dc  3242  pwssunim  4021  ordtriexmid  4247  ordtri2orexmid  4248  ontr2exmid  4250  onsucsssucexmid  4252  onsucelsucexmid  4255  ordsoexmid  4286  0elsucexmid  4289  ordpwsucexmid  4294  ordtri2or2exmid  4296  funcnvuni  4968  oprabidlem  5536  2oconcl  6022  zeo  8343
  Copyright terms: Public domain W3C validator