Theorem orim2i 711

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

Syntax hints:   -> wi 4   \/ wo 662

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 663

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  orbi2i  712  pm1.5  715  pm2.3  725  ordi  763  dcn  780  pm2.25dc  826  dcan  876  axi12  1448  dveeq2or  1738  equs5or  1752  sb4or  1755  sb4bor  1757  nfsb2or  1759  sbequilem  1760  sbequi  1761  sbal1yz  1919  dvelimor  1936  exmodc  1992  r19.44av  2514  elsuci  4166  acexmidlemcase  5538  zindd  8546