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

Theorem orim12i 749
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 723 . 2 (𝜑 → (𝜓𝜃))
3 orim12i.2 . . 3 (𝜒𝜃)
43olcd 724 . 2 (𝜒 → (𝜓𝜃))
52, 4jaoi 706 1 ((𝜑𝜒) → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wo 698
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 699
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  orim1i  750  orim2i  751  dcim  827  pm5.12dc  896  pm5.14dc  897  pm5.55dc  899  pm5.54dc  904  prlem2  959  xordc1  1375  19.43  1608  eueq3dc  2886  inssun  3348  abvor0dc  3418  ifmdc  3543  undifexmid  4156  pwssunim  4246  ordtriexmid  4482  ontriexmidim  4483  ordtri2orexmid  4484  ontr2exmid  4486  onsucsssucexmid  4488  onsucelsucexmid  4491  ordsoexmid  4523  0elsucexmid  4526  ordpwsucexmid  4531  ordtri2or2exmid  4532  ontri2orexmidim  4533  funcnvuni  5241  oprabidlem  5854  2oconcl  6388  inffiexmid  6853  unfiexmid  6864  ctssexmid  7095  exmidonfinlem  7130  sup3exmid  8833  zeo  9274  ef0lem  11568
  Copyright terms: Public domain W3C validator