Theorem orim2i 678

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

Syntax hints:   -> wi 4   \/ wo 629

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  orbi2i  679  pm1.5  682  pm2.3  692  ordi  729  dcn  746  pm2.25dc  792  dcan  842  axi12  1407  dveeq2or  1697  equs5or  1711  sb4or  1714  sb4bor  1716  nfsb2or  1718  sbequilem  1719  sbequi  1720  sbal1yz  1877  dvelimor  1894  exmodc  1950  r19.44av  2469  elsuci  4140  acexmidlemcase  5507  zindd  8356