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

Theorem orim12i 759
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 733 . 2 (𝜑 → (𝜓𝜃))
3 orim12i.2 . . 3 (𝜒𝜃)
43olcd 734 . 2 (𝜒 → (𝜓𝜃))
52, 4jaoi 716 1 ((𝜑𝜒) → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wo 708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  orim1i  760  orim2i  761  dcim  841  pm5.12dc  910  pm5.14dc  911  pm5.55dc  913  pm5.54dc  918  prlem2  974  xordc1  1393  19.43  1628  eueq3dc  2912  inssun  3376  abvor0dc  3447  ifmdc  3575  undifexmid  4194  pwssunim  4285  ordtriexmid  4521  ontriexmidim  4522  ordtri2orexmid  4523  ontr2exmid  4525  onsucsssucexmid  4527  onsucelsucexmid  4530  ordsoexmid  4562  0elsucexmid  4565  ordpwsucexmid  4570  ordtri2or2exmid  4571  ontri2orexmidim  4572  funcnvuni  5286  oprabidlem  5906  2oconcl  6440  inffiexmid  6906  unfiexmid  6917  ctssexmid  7148  exmidonfinlem  7192  sup3exmid  8914  zeo  9358  ef0lem  11668
  Copyright terms: Public domain W3C validator