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

Theorem orim12i 675
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 651 . 2 (φ → (ψ θ))
3 orim12i.2 . . 3 (χθ)
43olcd 652 . 2 (χ → (ψ θ))
52, 4jaoi 635 1 ((φ χ) → (ψ θ))
Colors of variables: wff set class
Syntax hints:  wi 4   wo 628
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 629
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  orim1i  676  orim2i  677  dcim  783  pm5.12dc  815  pm5.14dc  816  pm5.55dc  818  pm5.54dc  826  prlem2  880  xordc1  1281  19.43  1516  eueq3dc  2709  inssun  3171  abvor0dc  3236  pwssunim  4012  ordtriexmid  4210  ordtri2orexmid  4211  onsucsssucexmid  4212  onsucelsucexmid  4215  ordsoexmid  4240  ordpwsucexmid  4246  funcnvuni  4911  oprabidlem  5479  2oconcl  5961  zeo  8099
  Copyright terms: Public domain W3C validator