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

Theorem orim2i 678
 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 676 1 ((𝜒𝜑) → (𝜒𝜓))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∨ wo 629 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 630 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  orbi2i  679  pm1.5  682  pm2.3  692  ordi  729  dcn  746  pm2.25dc  792  dcan  842  axi12  1407  dveeq2or  1697  equs5or  1711  sb4or  1714  sb4bor  1716  nfsb2or  1718  sbequilem  1719  sbequi  1720  sbal1yz  1877  dvelimor  1894  exmodc  1950  r19.44av  2469  elsuci  4140  acexmidlemcase  5507  zindd  8356
 Copyright terms: Public domain W3C validator