Theorem orim2i 710

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 708	1 |- ( ( ch \/ ph ) -> ( ch \/ ps ) )

Syntax hints:   -> wi 4   \/ wo 661

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 662

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  orbi2i  711  pm1.5  714  pm2.3  724  ordi  762  dcn  779  pm2.25dc  825  dcan  875  axi12  1447  dveeq2or  1737  equs5or  1751  sb4or  1754  sb4bor  1756  nfsb2or  1758  sbequilem  1759  sbequi  1760  sbal1yz  1918  dvelimor  1935  exmodc  1991  r19.44av  2513  elsuci  4158  acexmidlemcase  5527  zindd  8465