Theorem orim2i 766

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

Syntax hints:   -> wi 4   \/ wo 713

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi2i  767  pm1.5  770  pm2.3  780  ordi  821  dcn  847  pm2.25dc  898  dcand  938  axi12  1560  dveeq2or  1862  equs5or  1876  sb4or  1879  sb4bor  1881  nfsb2or  1883  sbequilem  1884  sbequi  1885  sbal1yz  2052  dvelimor  2069  exmodc  2128  r19.44av  2690  exmidundif  4289  exmidundifim  4290  exmid1stab  4291  elsuci  4493  acexmidlemcase  5995  undifdcss  7081  updjudhf  7242  ctssdccl  7274  zindd  9561  fiubm  11045  lswex  11118  fsumsplitsn  11916  fprodcllem  12112  fprodsplitsn  12139  gsumwsubmcl  13524  gsumwmhm  13526  subctctexmid  16325