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

Theorem orim2i 735
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 733 1  |-  ( ( ch  \/  ph )  ->  ( ch  \/  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 682
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 683
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  orbi2i  736  pm1.5  739  pm2.3  749  ordi  790  dcn  812  pm2.25dc  863  dcan  903  axi12  1479  dveeq2or  1772  equs5or  1786  sb4or  1789  sb4bor  1791  nfsb2or  1793  sbequilem  1794  sbequi  1795  sbal1yz  1954  dvelimor  1971  exmodc  2027  r19.44av  2567  exmidundif  4099  exmidundifim  4100  elsuci  4295  acexmidlemcase  5737  undifdcss  6779  updjudhf  6932  ctssdccl  6964  zindd  9137  fsumsplitsn  11147  exmid1stab  13122  subctctexmid  13123
  Copyright terms: Public domain W3C validator