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

Theorem orim2i 713
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 711 1 ((𝜒𝜑) → (𝜒𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wo 664
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  orbi2i  714  pm1.5  717  pm2.3  727  ordi  765  dcn  784  pm2.25dc  830  dcan  880  axi12  1452  dveeq2or  1744  equs5or  1758  sb4or  1761  sb4bor  1763  nfsb2or  1765  sbequilem  1766  sbequi  1767  sbal1yz  1925  dvelimor  1942  exmodc  1998  r19.44av  2526  exmidundif  4026  elsuci  4221  acexmidlemcase  5629  undifdcss  6613  updjudhf  6749  zindd  8834  fsumsplitsn  10767
  Copyright terms: Public domain W3C validator