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

Theorem orim2i 665
Description: Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
Hypothesis
Ref Expression
orim1i.1 (φψ)
Assertion
Ref Expression
orim2i ((χ φ) → (χ ψ))

Proof of Theorem orim2i
StepHypRef Expression
1 id 19 . 2 (χχ)
2 orim1i.1 . 2 (φψ)
31, 2orim12i 663 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:  orbi2i  666  pm1.5  669  pm2.3  679  ordi  717  dcn  737  pm2.25dc  785  dcan  830  axi12  1388  dveeq2or  1679  equs5or  1693  sb4or  1696  sb4bor  1698  nfsb2or  1700  sbequilem  1701  sbequi  1702  sbal1yz  1859  dvelimor  1876  exmodc  1932  r19.44av  2447  elsuci  4089  acexmidlemcase  5431
  Copyright terms: Public domain W3C validator