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

Theorem orim2i 688
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 686 1 ((𝜒𝜑) → (𝜒𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wo 639
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  orbi2i  689  pm1.5  692  pm2.3  702  ordi  740  dcn  757  pm2.25dc  803  dcan  853  axi12  1423  dveeq2or  1713  equs5or  1727  sb4or  1730  sb4bor  1732  nfsb2or  1734  sbequilem  1735  sbequi  1736  sbal1yz  1893  dvelimor  1910  exmodc  1966  r19.44av  2486  elsuci  4168  acexmidlemcase  5535  zindd  8415
  Copyright terms: Public domain W3C validator