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

Theorem orim12i 663
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 639 . 2 (φ → (ψ θ))
3 orim12i.2 . . 3 (χθ)
43olcd 640 . 2 (χ → (ψ θ))
52, 4jaoi 623 1 ((φ χ) → (ψ θ))
Colors of variables: wff set class
Syntax hints:  wi 4   wo 616
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 617
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  orim1i  664  orim2i  665  dcim  772  pm5.12dc  804  pm5.14dc  805  pm5.55dc  807  pm5.54dc  815  prlem2  867  xordc1  1265  19.43  1497  eueq3dc  2688  inssun  3150  abvor0dc  3215  pwssunim  3991  ordtriexmid  4190  ordtri2orexmid  4191  onsucsssucexmid  4192  onsucelsucexmid  4195  ordsoexmid  4220  ordpwsucexmid  4226  funcnvuni  4890  oprabidlem  5456  2oconcl  5933
  Copyright terms: Public domain W3C validator