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

Theorem orim2i 733
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 731 1  |-  ( ( ch  \/  ph )  ->  ( ch  \/  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 680
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 681
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  orbi2i  734  pm1.5  737  pm2.3  747  ordi  788  dcn  810  pm2.25dc  861  dcan  901  axi12  1477  dveeq2or  1770  equs5or  1784  sb4or  1787  sb4bor  1789  nfsb2or  1791  sbequilem  1792  sbequi  1793  sbal1yz  1952  dvelimor  1969  exmodc  2025  r19.44av  2565  exmidundif  4097  exmidundifim  4098  elsuci  4293  acexmidlemcase  5735  undifdcss  6777  updjudhf  6930  ctssdccl  6962  zindd  9123  fsumsplitsn  11130  exmid1stab  13029  subctctexmid  13030
  Copyright terms: Public domain W3C validator