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

Theorem orim12i 755
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 729 . 2 (𝜑 → (𝜓𝜃))
3 orim12i.2 . . 3 (𝜒𝜃)
43olcd 730 . 2 (𝜒 → (𝜓𝜃))
52, 4jaoi 712 1 ((𝜑𝜒) → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wo 704
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 705
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  orim1i  756  orim2i  757  dcim  837  pm5.12dc  906  pm5.14dc  907  pm5.55dc  909  pm5.54dc  914  prlem2  970  xordc1  1389  19.43  1622  eueq3dc  2905  inssun  3368  abvor0dc  3439  ifmdc  3566  undifexmid  4180  pwssunim  4270  ordtriexmid  4506  ontriexmidim  4507  ordtri2orexmid  4508  ontr2exmid  4510  onsucsssucexmid  4512  onsucelsucexmid  4515  ordsoexmid  4547  0elsucexmid  4550  ordpwsucexmid  4555  ordtri2or2exmid  4556  ontri2orexmidim  4557  funcnvuni  5269  oprabidlem  5888  2oconcl  6422  inffiexmid  6888  unfiexmid  6899  ctssexmid  7130  exmidonfinlem  7174  sup3exmid  8877  zeo  9321  ef0lem  11627
  Copyright terms: Public domain W3C validator