Theorem orim2i 763

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

Syntax hints:   -> wi 4   \/ wo 710

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi2i  764  pm1.5  767  pm2.3  777  ordi  818  dcn  844  pm2.25dc  895  dcand  935  axi12  1537  dveeq2or  1839  equs5or  1853  sb4or  1856  sb4bor  1858  nfsb2or  1860  sbequilem  1861  sbequi  1862  sbal1yz  2029  dvelimor  2046  exmodc  2104  r19.44av  2665  exmidundif  4250  exmidundifim  4251  exmid1stab  4252  elsuci  4450  acexmidlemcase  5939  undifdcss  7020  updjudhf  7181  ctssdccl  7213  zindd  9491  fiubm  10973  fsumsplitsn  11721  fprodcllem  11917  fprodsplitsn  11944  gsumwsubmcl  13328  gsumwmhm  13330  subctctexmid  15937