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

Theorem orim12i 731
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 705 . 2 (𝜑 → (𝜓𝜃))
3 orim12i.2 . . 3 (𝜒𝜃)
43olcd 706 . 2 (𝜒 → (𝜓𝜃))
52, 4jaoi 688 1 ((𝜑𝜒) → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wo 680
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 681
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  orim1i  732  orim2i  733  dcim  809  pm5.12dc  878  pm5.14dc  879  pm5.55dc  881  pm5.54dc  886  prlem2  941  xordc1  1354  19.43  1590  eueq3dc  2829  inssun  3284  abvor0dc  3354  ifmdc  3477  undifexmid  4085  pwssunim  4174  ordtriexmid  4405  ordtri2orexmid  4406  ontr2exmid  4408  onsucsssucexmid  4410  onsucelsucexmid  4413  ordsoexmid  4445  0elsucexmid  4448  ordpwsucexmid  4453  ordtri2or2exmid  4454  funcnvuni  5160  oprabidlem  5768  2oconcl  6302  inffiexmid  6766  unfiexmid  6772  ctssexmid  6990  sup3exmid  8675  zeo  9110  ef0lem  11276
  Copyright terms: Public domain W3C validator