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  1865  equs5or  1879  sb4or  1882  sb4bor  1884  nfsb2or  1886  sbequilem  1887  sbequi  1888  sbal1yz  2055  dvelimor  2072  exmodc  2131  r19.44av  2702  exmidundif  4319  exmidundifim  4320  exmid1stab  4321  elsuci  4524  acexmidlemcase  6045  undifdcss  7183  updjudhf  7370  ctssdccl  7402  zindd  9696  fiubm  11195  lswex  11276  fsumsplitsn  12096  fprodcllem  12292  fprodsplitsn  12319  gsumwsubmcl  13709  gsumwmhm  13711  subctctexmid  16774