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

Theorem orim2i 677
 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 675 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:  orbi2i  678  pm1.5  681  pm2.3  691  ordi  728  dcn  745  pm2.25dc  791  dcan  841  axi12  1404  dveeq2or  1694  equs5or  1708  sb4or  1711  sb4bor  1713  nfsb2or  1715  sbequilem  1716  sbequi  1717  sbal1yz  1874  dvelimor  1891  exmodc  1947  r19.44av  2463  elsuci  4106  acexmidlemcase  5450  zindd  8132
 Copyright terms: Public domain W3C validator