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

Theorem orim2i 751
 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 749 1 ((𝜒𝜑) → (𝜒𝜓))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∨ wo 698 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  orbi2i  752  pm1.5  755  pm2.3  765  ordi  806  dcn  828  pm2.25dc  879  dcan  919  axi12  1491  dveeq2or  1793  equs5or  1807  sb4or  1810  sb4bor  1812  nfsb2or  1814  sbequilem  1815  sbequi  1816  sbal1yz  1978  dvelimor  1995  exmodc  2053  r19.44av  2613  exmidundif  4162  exmidundifim  4163  elsuci  4358  acexmidlemcase  5809  undifdcss  6856  updjudhf  7009  ctssdccl  7041  zindd  9261  fsumsplitsn  11284  fprodcllem  11480  fprodsplitsn  11507  exmid1stab  13511  subctctexmid  13512
 Copyright terms: Public domain W3C validator