Theorem orim2i 769

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

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ch -> ch )
2		orim1i.1	. 2 |- ( ph -> ps )
3	1, 2	orim12i 767	1 |- ( ( ch \/ ph ) -> ( ch \/ ps ) )

Syntax hints:   -> wi 4   \/ wo 716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi2i  770  pm1.5  773  pm2.3  783  ordi  824  dcn  850  pm2.25dc  901  dcand  941  axi12  1563  dveeq2or  1864  equs5or  1878  sb4or  1881  sb4bor  1883  nfsb2or  1885  sbequilem  1886  sbequi  1887  sbal1yz  2054  dvelimor  2071  exmodc  2130  r19.44av  2693  exmidundif  4302  exmidundifim  4303  exmid1stab  4304  elsuci  4506  acexmidlemcase  6023  undifdcss  7158  updjudhf  7321  ctssdccl  7353  zindd  9642  fiubm  11138  lswex  11214  fsumsplitsn  12034  fprodcllem  12230  fprodsplitsn  12257  gsumwsubmcl  13642  gsumwmhm  13644  subctctexmid  16705