Theorem orim2i 751

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

Syntax hints:   -> wi 4   \/ wo 698

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orbi2i  752  pm1.5  755  pm2.3  765  ordi  806  dcn  828  pm2.25dc  879  dcan  919  axi12  1494  dveeq2or  1796  equs5or  1810  sb4or  1813  sb4bor  1815  nfsb2or  1817  sbequilem  1818  sbequi  1819  sbal1yz  1981  dvelimor  1998  exmodc  2056  r19.44av  2616  exmidundif  4166  exmidundifim  4167  elsuci  4362  acexmidlemcase  5813  undifdcss  6860  updjudhf  7013  ctssdccl  7045  zindd  9265  fsumsplitsn  11289  fprodcllem  11485  fprodsplitsn  11512  exmid1stab  13533  subctctexmid  13534