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

Theorem orim2i 761
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 759 1 ((𝜒𝜑) → (𝜒𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wo 708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  orbi2i  762  pm1.5  765  pm2.3  775  ordi  816  dcn  842  pm2.25dc  893  dcan  933  axi12  1514  dveeq2or  1816  equs5or  1830  sb4or  1833  sb4bor  1835  nfsb2or  1837  sbequilem  1838  sbequi  1839  sbal1yz  2001  dvelimor  2018  exmodc  2076  r19.44av  2636  exmidundif  4206  exmidundifim  4207  exmid1stab  4208  elsuci  4403  acexmidlemcase  5869  undifdcss  6921  updjudhf  7077  ctssdccl  7109  zindd  9370  fiubm  10807  fsumsplitsn  11417  fprodcllem  11613  fprodsplitsn  11640  subctctexmid  14720
  Copyright terms: Public domain W3C validator