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

Theorem orim2i 711
Description: Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
Hypothesis
Ref Expression
orim1i.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
orim2i  |-  ( ( ch  \/  ph )  ->  ( ch  \/  ps ) )

Proof of Theorem orim2i
StepHypRef Expression
1 id 19 . 2  |-  ( ch 
->  ch )
2 orim1i.1 . 2  |-  ( ph  ->  ps )
31, 2orim12i 709 1  |-  ( ( ch  \/  ph )  ->  ( ch  \/  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 662
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 663
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  orbi2i  712  pm1.5  715  pm2.3  725  ordi  763  dcn  780  pm2.25dc  826  dcan  876  axi12  1448  dveeq2or  1738  equs5or  1752  sb4or  1755  sb4bor  1757  nfsb2or  1759  sbequilem  1760  sbequi  1761  sbal1yz  1919  dvelimor  1936  exmodc  1992  r19.44av  2514  elsuci  4166  acexmidlemcase  5538  zindd  8546
  Copyright terms: Public domain W3C validator